2be0cf8 · Idris-dev · git.iko.soy

CHANGELOG+8−1

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

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

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

3434 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.

3643

3744New in 0.9.16:

3845--------------

Setup.hs+9−2

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

5757 Just False -> False

5858 Nothing -> True

5959

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+

6067isRelease :: S.ConfigFlags -> Bool

6168isRelease flags =

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

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

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

177184 return (Just buildinfo, [])

178185

179−idrisBuild _ flags _ local = do

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

180187 buildStdLib

181188 buildRTS

182189 where

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

199206-- -----------------------------------------------------------------------------

200207-- Copy/Install

201208

202−idrisInstall verbosity copy pkg local = do

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

203210 installStdLib

204211 installRTS

205212 where

benchmarks/quasigroups/Main.idr+2−2

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

1414 Left err => putStrLn err

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

1616 putStrLn "Got board:"

17− print board

17+ printLn board

1818 putStrLn "Solving..."

1919 case fillBoard board legal of

2020 Nothing => putStrLn "No solution found"

2121 Just (solved ** _) => do

2222 putStrLn "Solution found:"

23− print solved

23+ printLn solved

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

benchmarks/trivial/sortvec.idr+2−3

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

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

1414

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

16−mkSortVec Z = return []

16+mkSortVec Z = return []

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

1818

1919main : IO ()

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

2121-- let arg = "2000"

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

2323 putStrLn "Made vector"

24− print (vsort vec)

25−

24+ printLn (vsort vec)

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

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

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

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

99 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

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

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

1313 exec_db_v2 stmt -- execute the prepared query

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

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

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

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

1717 close_db db -- close the datbase

1818 return ()

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

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

2323 let x = (fst sql)

2424 let list = (snd sql)

25− liftIO(print x)

25+ liftIO(printLn x)

2626 stmt <- (prepare_db db x)

2727 bindMulti stmt list

2828 exec_db_v2 stmt

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

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

3636 let x = (fst sql)

3737 let list = (snd sql)

38− liftIO(print x)

38+ liftIO(printLn x)

3939 stmt <- (prepare_db db x)

4040 bindMulti stmt list

4141 exec_db_v2 stmt

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

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

4949 let x = (fst sql)

5050 let list = (snd sql)

51− liftIO(print x)

51+ liftIO(printLn x)

5252 stmt <- (prepare_db db x)

5353 bindMulti stmt list

5454 exec_db_v2 stmt

5555 res <- toList_v1 db

56− liftIO(print res)

56+ liftIO(printLn res)

5757 finalize_db stmt

5858 close_db db

5959 return ()

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

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

6565 let x = (fst sql)

6666 let list = (snd sql)

67− liftIO(print x)

67+ liftIO(printLn x)

6868 stmt <- (prepare_db db x)

6969 bindMulti stmt list

7070 exec_db_v2 stmt

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

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

7979 let x = (fst sql)

8080 let list = (snd sql)

81− liftIO(print x)

81+ liftIO(printLn x)

8282 stmt <- (prepare_db db x)

8383 bindMulti stmt list

8484 exec_db_v2 stmt

8585 res <- toList_v1 db

86− liftIO(print res)

86+ liftIO(printLn res)

8787 finalize_db stmt

8888 close_db db

8989 return ()

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

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

9595 let x = (fst sql)

9696 let list = (snd sql)

97− liftIO(print x)

97+ liftIO(printLn x)

9898 stmt <- (prepare_db db x)

9999 bindMulti stmt list

100100 exec_db_v2 stmt

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

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

109109 let x = (fst sql)

110110 let list = (snd sql)

111− liftIO(print x)

111+ liftIO(printLn x)

112112 stmt <- (prepare_db db x)

113113 bindMulti stmt list

114114 exec_db_v2 stmt

115115 res <- toList_v1 db

116− liftIO(print res)

116+ liftIO(printLn res)

117117 finalize_db stmt

118118 close_db db

119119 return ()

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

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

124124 let x = (fst sql)

125125 let list = (snd sql)

126− liftIO(print x)

126+ liftIO(printLn x)

127127 stmt <- (prepare_db db x)

128128 bindMulti stmt list

129129 exec_db_v2 stmt

130130 res <- toList_v1 db

131− liftIO(print res)

131+ liftIO(printLn res)

132132 finalize_db stmt

133133 close_db db

134134 return ()

idris.cabal+9

@@ -293,6 +293,9 @@ Extra-source-files:

293293 test/reg058/run

294294 test/reg058/*.idr

295295 test/reg058/expected

296+ test/reg059/run

297+ test/reg059/*.idr

298+ test/reg059/expected

296299

297300 test/basic001/run

298301 test/basic001/*.idr

@@ -662,6 +665,11 @@ Flag CI

662665 Default: False

663666 manual: True

664667

668+Flag execonly

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

670+ Default: False

671+ manual: True

672+

665673Library

666674 hs-source-dirs: src

667675 Exposed-modules:

@@ -729,6 +737,7 @@ Library

729737 , Idris.ProofSearch

730738 , Idris.Prover

731739 , Idris.Providers

740+ , Idris.Reflection

732741 , Idris.REPL

733742 , Idris.REPLParser

734743 , Idris.Transforms

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

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

66%access public

77

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

1010 ||| Get the context

1111 get : m s

1212 ||| Write a new context/output

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

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

5151

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

5353listens : 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)

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

5657 return (a, f' w)

5758

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

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

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

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

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

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

182+ , TermPart `(Integer : Type)

183183 ]

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

185185 = mkFinIntegerErr n m

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

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

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

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

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

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

275276 show UniverseError = "UniverseError"

276277 show ProgramLineComment = "ProgramLineComment"

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

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

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

146146isEmptySizeZero Empty p = Refl

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

148148

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

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

150150emptyHeapValid = Refl

151151

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

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

182182 does seem to work correctly!

183183main : IO ()

184184main = do

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

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

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

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

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

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

188188 return ()

189189-}

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

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

3636 eq (f a) (f b)

3737

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

39−minimum x y with (order x y)

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

4040 | Left _ = x

4141 | Right _ = y

4242

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

44−maximum x y with (order x y)

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

4545 | Left _ = y

4646 | Right _ = x

4747

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

103103decideLTE Z y = Yes LTEZero

104104decideLTE (S x) Z = No zeroNeverGreater

105105decideLTE (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))

107107 | No _ with (decideLTE x y)

108108 | Yes nLTEm = Yes (LTESucc nLTEm)

109109 | No nGTm = No (ltesuccinjective nGTm)

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

122122instance Ordered Nat LTE where

123123 order Z n = Left LTEZero

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

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

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

128128

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

@@ -4,7 +4,7 @@ import Effects

44import System

55import Control.IOExcept

66

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

88 Raise : a -> { () } Exception a b

99

1010instance Handler (Exception a) Maybe where

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

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

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

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

3030raise err = call $ Raise err

3131

3232

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

3939

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

4141-- handler can be introduced mid interpretation?

42−

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

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

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

4343putStr s = call $ PutStr s

4444

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

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

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

48+

4549||| Write a character to standard output.

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

4751putChar c = call $ PutCh c

4852

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

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

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

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

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

55+putCharLn c = putStrLn (singleton c)

5256

5357||| Read a string from standard input.

5458getStr : { [STDIO] } Eff String

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

@@ -4,7 +4,7 @@ import Effects

44import System

55import Control.IOExcept

66

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

88 Raise : a -> { () } Exception a b

99

1010instance Handler (Exception a) Maybe where

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

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

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

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

3030raise err = call $ Raise err

3131

3232

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

3939

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

4141-- handler can be introduced mid interpretation?

42−

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

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

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

417417

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

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

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

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

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

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

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

422422

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

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

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

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

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

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

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

427427

428428instance Quotable TTName TT where

429429 quotedTy = `(TTName)

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

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

3131 | CantResolve TT

3232 | CantResolveAlts (List TTName)

3333 | IncompleteTerm TT

34+ | NoEliminator String TT

3435 | UniverseError

3536 | ProgramLineComment

3637 | Inaccessible TTName

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

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

88import Prelude.Monad

99import Language.Reflection

1010

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+

1119abstract

1220data Tactical : Type -> Type where

1321 -- obligatory control stuff

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

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

4048 prim__Intro : Maybe TTName -> Tactical ()

4149

50+ prim__DeclareType : TyDecl -> Tactical ()

51+

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

4353

54+

4455-------------

4556-- Public API

4657-------------

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

117128rewriteWith : Raw -> Tactical ()

118129rewriteWith rule = prim__Rewrite rule

119130

131+declareType : TyDecl -> Tactical ()

132+declareType decl = prim__DeclareType decl

133+

120134debug : Tactical a

121135debug = prim__Debug Nothing

122136

libs/prelude/Prelude.idr+15−5

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

442442putStrLn : String -> IO' ffi ()

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

444444

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

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

446446partial

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

448−print x = putStrLn (show x)

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

453+printLn x = putStrLn (show x)

449454

450455||| Read one line of input from stdin

451456partial

452457getLine : IO' ffi String

453−getLine = prim_read

458+getLine = prim_read

454459

455460||| Write a single character to stdout

456461partial

457462putChar : 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)

459469

460470||| Read a single character from stdin

461471partial

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

484494do_fopen : String -> String -> IO Ptr

485495do_fopen f m

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

487−

497+

488498||| Open a file

489499||| @ f the filename

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

316316

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

318318 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

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

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

322322

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

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

3131

3232||| Function composition

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

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

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

3535

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

3737||| @ f the function to flip

samples/binary.idr+1−2

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

4141main : IO ()

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

4343 let n2 = zero # b1 # b1 # b1 # b0

44− print (adc n1 n2 b0)

44+ printLn (adc n1 n2 b0)

4545

4646

4747

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

9292 rewrite sym (plusZeroRightNeutral c) ;

9393 trivial;

9494}

95−

samples/interp-alt.idr+2−2

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

7777testFac = interp [] eFac 4

7878

7979main : IO ()

80−main = do print test

81− print testFac

80+main = do printLn test

81+ printLn testFac

samples/interp.idr+1−2

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

8888testFac = interp [] eFac 4

8989

9090main : IO ()

91−main = print testFac

92−

91+main = printLn testFac

samples/javaffi.idr+1−1

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

99main : IO ()

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

1111 res <- binom 49 6

12− print res

12+ printLn res

src/Idris/AbsSyntax.hs+47−23

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

360360addInstance int n i

361361 = do ist <- getIState

362362 case lookupCtxt n (idris_classes ist) of

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

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

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

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

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

367367 putIState $ ist { idris_classes = cs }

368368 where addI i ins | int = i : ins

369369 | chaser n = ins ++ [i]

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

455455putIState :: IState -> Idris ()

456456putIState = put

457457

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

459+updateIState f = do i <- getIState

460+ putIState $ f i

461+

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

459463withContext ctx name dflt action = do

460464 ist <- getIState

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

547551addDeferred = addDeferred' Ref

548552addDeferredTyCon = addDeferred' (TCon 0 0)

549553

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

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

555+addDeferred' :: NameType

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

551564addDeferred' nt ns

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

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

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

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

10771090 = 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)

10791092 = PClass doc info f

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

10811094 n

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

10831096 pDocs

1097+ fds

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

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

10861100 = PInstance doc argDocs info f

@@ -1467,31 +1481,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

14671481

14681482-- Add implicit arguments in function calls

14691483addImplPat :: IState -> PTerm -> PTerm

1470−addImplPat = addImpl' True [] []

1484+addImplPat = addImpl' True [] [] []

14711485

14721486addImplBound :: IState -> [Name] -> PTerm -> PTerm

1473−addImplBound ist ns = addImpl' False ns [] ist

1487+addImplBound ist ns = addImpl' False ns [] [] ist

14741488

14751489addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

1476−addImplBoundInf ist ns inf = addImpl' False ns inf ist

1490+addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

14771491

14781492-- | Add the implicit arguments to applications in the term

1479−addImpl :: IState -> PTerm -> PTerm

1493+-- [Name] gives the names to always expend, even when under a binder of

1494+-- that name (this is to expand methods with implicit arguments in dependent

1495+-- type classes).

1496+addImpl :: [Name] -> IState -> PTerm -> PTerm

14801497addImpl = addImpl' False [] []

14811498

14821499-- TODO: in patterns, don't add implicits to function names guarded by constructors

14831500-- and *not* inside a PHidden

14841501

1485−addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1486−addImpl' inpat env infns ist ptm

1502+addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1503+addImpl' inpat env infns imp_meths ist ptm

14871504 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

14881505 where

14891506 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

14901507 ai qq env ds (PRef fc f)

14911508 | f `elem` infns = PInferRef fc f

1492− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1509+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []

14931510 ai qq env ds (PHidden (PRef fc f))

1494− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])

1511+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])

14951512 ai qq env ds (PEq fc lt rt l r)

14961513 = let lt' = ai qq env ds lt

14971514 rt' = ai qq env ds rt

@@ -1527,7 +1544,7 @@ addImpl' inpat env infns ist ptm

15271544 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

15281545 | not (f `elem` map fst env)

15291546 = let as' = map (fmap (ai qq env ds)) as in

1530− handleErr $ aiFn inpat False qq ist fc f ds as'

1547+ handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'

15311548 | Just (Just ty) <- lookup f env =

15321549 let as' = map (fmap (ai qq env ds)) as

15331550 arity = getPArity ty in

@@ -1562,7 +1579,9 @@ addImpl' inpat env infns ist ptm

15621579 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

15631580 ai qq env ds (PPi p n ty sc)

15641581 = let ty' = ai qq env ds ty

1565− sc' = ai qq ((n, Just ty):env) ds sc in

1582+ env' = if n `elem` imp_meths then env

1583+ else ((n, Just ty) : env)

1584+ sc' = ai qq env' ds sc in

15661585 PPi p n ty' sc'

15671586 ai qq env ds (PGoal fc r n sc)

15681587 = let r' = ai qq env ds r

@@ -1586,8 +1605,8 @@ addImpl' inpat env infns ist ptm

15861605-- if in a pattern, and there are no arguments, and there's no possible

15871606-- names with zero explicit arguments, don't add implicits.

15881607

1589−aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1590−aiFn inpat True qq ist fc f ds []

1608+aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1609+aiFn inpat True qq imp_meths ist fc f ds []

15911610 = case lookupDef f (tt_ctxt ist) of

15921611 [] -> Right $ PPatvar fc f

15931612 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1595,7 +1614,7 @@ aiFn inpat True qq ist fc f ds []

15951614 if (not (vname f) || tcname f

15961615 || any (conCaf (tt_ctxt ist)) ialts)

15971616-- any constructor alts || any allImp ialts))

1598− then aiFn inpat False qq ist fc f ds [] -- use it as a constructor

1617+ then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor

15991618 else Right $ PPatvar fc f

16001619 where imp (PExp _ _ _ _) = False

16011620 imp _ = True

@@ -1609,9 +1628,9 @@ aiFn inpat True qq ist fc f ds []

16091628 vname (UN n) = True -- non qualified

16101629 vname _ = False

16111630

1612−aiFn inpat expat qq ist fc f ds as

1631+aiFn inpat expat qq imp_meths ist fc f ds as

16131632 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1614−aiFn inpat expat qq ist fc f ds as

1633+aiFn inpat expat qq imp_meths ist fc f ds as

16151634 -- This is where namespaces get resolved by adding PAlternative

16161635 = do let ns = lookupCtxtName f (idris_implicits ist)

16171636 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1619,15 +1638,20 @@ aiFn inpat expat qq ist fc f ds as

16191638 [] -> nh

16201639 x -> x

16211640 case ns' of

1622− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1641+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)

16231642 [] -> if f `elem` (map fst (idris_metavars ist))

16241643 then Right $ PApp fc (PRef fc f) as

16251644 else Right $ mkPApp fc (length as) (PRef fc f) as

16261645 alts -> Right $

16271646 PAlternative True $

1628− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1647+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))

16291648 (insertImpl ns as)) alts

16301649 where

1650+ -- if the name is in imp_meths, we should actually refer to the bound

1651+ -- name rather than the global one after expanding implicits

1652+ isImpName f f' | f `elem` imp_meths = f

1653+ | otherwise = f'

1654+

16311655 trimAlts [] alts = alts

16321656 trimAlts ns alts

16331657 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

@@ -1671,7 +1695,7 @@ aiFn inpat expat qq ist fc f ds as

16711695 PImp p True l n Placeholder :

16721696 insImpAcc (M.insert n Placeholder pnas) ps given imps

16731697 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1674− let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1698+ let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in

16751699 case find n imps [] of

16761700 Just (tm, imps') ->

16771701 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+20−9

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

184184 idris_name :: Int,

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

186186 -- ^ Full application LHS on source line

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

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

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

188192 idris_coercions :: [Name],

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

190194 syntax_rules :: SyntaxRules,

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

599603 Name

600604 [(Name, t)] -- parameters

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

606+ [Name] -- determining parameters

602607 [PDecl' t] -- declarations

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

604609 -- class name, parameters, method declarations

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

631636-- For elaborator state

632637data EState = EState {

633638 case_decls :: [PDecl],

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

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

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

635641 }

636642

637−initEState = EState [] []

643+initEState :: EState

644+initEState = EState [] [] []

638645

639646type ElabD a = Elab' EState a

640647

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

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

694701declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

698705declared (PDSL n _) = [n]

699706declared (PSyntax _ _) = []

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

712719tldeclared (PParams _ _ ds) = []

713720tldeclared (PMutual _ ds) = concatMap tldeclared ds

714721tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

717724tldeclared _ = []

718725

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

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

729736defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

733740defined (PDSL n _) = [n]

734741defined (PSyntax _ _) = []

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

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

10301037 class_default_superclasses :: [PDecl],

10311038 class_params :: [Name],

1032− class_instances :: [Name] }

1039+ class_instances :: [Name],

1040+ class_determiners :: [Int] }

10331041 deriving Show

10341042{-!

10351043deriving instance Binary ClassInfo

@@ -1190,6 +1198,9 @@ data SyntaxInfo = Syn { using :: [Using],

11901198 syn_params :: [(Name, PTerm)],

11911199 syn_namespace :: [String],

11921200 no_imp :: [Name],

1201+ imp_methods :: [Name], -- class methods. When expanding

1202+ -- implicits, these should be expanded even under

1203+ -- binders

11931204 decoration :: Name -> Name,

11941205 inPattern :: Bool,

11951206 implicitAllowed :: Bool,

@@ -1203,7 +1214,7 @@ deriving instance NFData SyntaxInfo

12031214deriving instance Binary SyntaxInfo

12041215!-}

12051216

1206−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0

1217+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0

12071218

12081219expandNS :: SyntaxInfo -> Name -> Name

12091220expandNS syn n@(NS _ _) = n

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

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

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

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

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

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

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

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

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

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

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

9191 put x

9292 put y

9393 put z

94− put (CantResolve t) = do putWord8 15

95− put t

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

95+ put t

9696 put (CantResolveAlts ns) = do putWord8 16

9797 put ns

9898 put (IncompleteTerm t) = do putWord8 17

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

146146 put x1

147147 put x2

148148 put x3

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

150+ put s

151+ put t

149152

150153 get = do i <- getWord8

151154 case i of

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

172175 13 -> fmap NoTypeDecl get

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

174177 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

176179 16 -> fmap CantResolveAlts get

177180 17 -> fmap IncompleteTerm get

178181 18 -> return UniverseError

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

205208 x2 <- get

206209 x3 <- get

207210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

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

209215----- Generated by 'derive'

210216

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

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

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

8181 rnf (NotInjective x1 x2 x3)

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

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

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

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

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

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

8687 rnf UniverseError = ()

8788 rnf ProgramLineComment = ()

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

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

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

756756

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

758758try' t1 t2 proofSearch

759− = do s <- get

760− ps <- get_probs

761− ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

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

764− return $! v

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

766− if recoverableErr e1 then

767− do case runStateT t2 s of

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

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

770− then lift (tfail e1)

771− else lift (tfail e2)

772− else lift (tfail e1)

759+ = do s <- get

760+ ps <- get_probs

761+ ulog <- getUnifyLog

762+ case prunStateT 999999 False ps t1 s of

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

764+ return $! v

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

766+ if recoverableErr e1 then

767+ do case runStateT t2 s of

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

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

770+ then lift (tfail e1)

771+ else lift (tfail e2)

772+ else lift (tfail e1)

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

774774 = -- traceWhen r (show err) $

775775 r || proofSearch

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

782782 recoverableErr (ElabDebug _ _ _) = False

783783 recoverableErr _ = True

784784

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+

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

786802tryWhen True a b = try a b

787803tryWhen False a b = a

src/Idris/Core/ProofState.hs+9−6

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

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

682682 let tmt' = normalise ctxt env tmt

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

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

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

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

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

686686 case unApply tmt' of

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

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

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

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

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

719719 return scv'

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

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

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

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

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

723+ tmt'

723724 where scname = sMN 0 "scarg"

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

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

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

878879 ctxt = context ps

879880 ulog = unifylog ps

880881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

881883

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

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

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

889891 if newx || newy || ready ||

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

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

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

893− up (ns ++ v) ps

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

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

896+ up (ns ++ v') ps

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

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

896899 (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

172172 else (t, False)

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

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

175178 updateSolved' xs t = (t, False)

176179

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

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

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

155155 | WithFnType t

156156 | NoTypeDecl Name

157157 | NotInjective t t t

158− | CantResolve t

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

159+ t

159160 | CantResolveAlts [Name]

160161 | IncompleteTerm t

162+ | NoEliminator String t

161163 | UniverseError

162164 | UniqueError Universe Name

163165 | UniqueKindError Universe Name

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

231233 size (NoSuchVariable name) = size name

232234 size (NoTypeDecl name) = size name

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

234− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

235237 size (NoRewriting trm) = size trm

236238 size (CantResolveAlts _) = 1

237239 size (IncompleteTerm trm) = size trm

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

246248

247249score :: Err -> Int

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

249−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

250252score (NoSuchVariable _) = 1000

251253score (ProofSearchFail e) = score e

252254score (CantSolveGoal _ _) = 100000

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

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

508510 concatMap (Map.toList) allns

509511

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

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

511513addAlist [] ctxt = ctxt

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

513515

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

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

935937instantiate :: TT n -> TT n -> TT n

936938instantiate e = subst 0 where

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

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

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

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

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

945948-- that has been substituted.

946949substV :: TT n -> TT n -> TT n

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

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

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

949953 | otherwise = V x

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

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

10381042 -- substitution happens...)

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

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

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

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

10431050 (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 =

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

101101 holeIn env f || f `elem` holes

102102 = 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)

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

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

106106 holeIn env f || f `elem` holes

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

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

111111 holeIn env f || f `elem` holes

112112 = 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)

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

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

116116 holeIn env f || f `elem` holes

src/Idris/Coverage.hs+1−1

@@ -24,7 +24,7 @@ import Control.Monad.State.Strict

2424-- provided explicitly from new clause generation.

2525mkPatTm :: PTerm -> Idris Term

2626mkPatTm t = do i <- getIState

27− let timp = addImpl' True [] [] i t

27+ let timp = addImpl' True [] [] [] i t

2828 evalStateT (toTT (mapPT deNS timp)) 0

2929 where

3030 toTT (PRef _ n) = do i <- lift getIState

src/Idris/DeepSeq.hs+6−6

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

149149 rnf x2 `seq`

150150 rnf x3 `seq`

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

153153 = rnf x1 `seq`

154154 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` ()

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

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

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

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

314314

315315instance NFData ClassInfo where

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

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

317317 = 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` ()

319319

320320instance NFData OptInfo where

321321 rnf (Optimise x1 x2)

@@ -353,10 +353,10 @@ instance NFData Using where

353353 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

354354

355355instance NFData SyntaxInfo where

356− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

356+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

357357 = rnf x1 `seq`

358358 rnf x2 `seq`

359359 rnf x3 `seq`

360360 rnf x4 `seq`

361361 rnf x5 `seq`

362− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

362+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

src/Idris/Delaborate.hs+7−1

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

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

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

291291 annTm y (pprintTerm i (delab i y))

292−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)

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

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

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

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

299299pprintErr' i (CantMatch t) =

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

301301pprintErr' 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."

302308pprintErr' i UniverseError = text "Universe inconsistency"

303309pprintErr' i (UniqueError NullType n)

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

src/Idris/Elab/Class.hs+38−20

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

5050

5151import Util.Pretty(pretty, text)

5252

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

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

5454

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

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

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

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

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

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

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

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

6061 let tty = pibind ps PType

6162 let constraint = PApp fc (PRef fc tn)

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

7576 let (methods, imethods)

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

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

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

7979 -- build instance constructor type

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

81− -- to elsewhere in the class declaration

8280 let cty = impbind ps $ conbind constraints

8381 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

8482 constraint

8583 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

8684 let ddecl = PDatadecl tn tty cons

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

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

86+ -- Elaborate the data declaration

87+ elabData info (syn { no_imp = no_imp syn ++ mnames,

88+ imp_methods = mnames }) doc pDocs fc [] ddecl

89+ dets <- findDets cn fds

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

91+

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

90− logLvl 5 $ "Building functions"

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

92−-- ++ using syn }

93− fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

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

93+ cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

94+ mapM_ (rec_elabDecl info EAll info) (concat cfns)

95+

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

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

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

99+ -- Elaborate the the top level methods

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

101+

98102 -- add the default definitions

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

100104 addIBC (IBCClass tn)

@@ -130,8 +134,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

130134

131135 getMName (PTy _ _ _ _ _ n _) = nsroot n

132136 tdecl allmeths (PTy doc _ syn _ o n t)

133− = do t' <- implicit' info syn allmeths n t

134− logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

137+ = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

138+ logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135139 return ( (n, (toExp (map fst ps) Exp t')),

136140 (n, (doc, o, (toExp (map fst ps)

137141 (\ l s p -> Imp l s p Nothing) t'))),

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

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

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

203207

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

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

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

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

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

207211 getMArgs _ = []

208212

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

210214 | otherwise = getMeth ms as x

211215

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

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

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

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

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

215219 lhsArgs [] _ = []

216220

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

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

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

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

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

220224 rhsArgs [] _ = []

221225

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

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

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

232236 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+35−23

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

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

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

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

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

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

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

459+ do setContext ctxt'

460+ processTacticDecls newDecls

461+ let lhs_tm = orderPats (getInferTerm lhs')

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

461463 OK _ -> return True

462464 err -> return False

@@ -546,7 +548,7 @@ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

546548elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

547549 = do let tcgen = Dictionary `elem` opts

548550 i <- get

549− let lhs = addImpl i lhs_in

551+ let lhs = addImpl [] i lhs_in

550552 b <- checkPossible info fc tcgen fname lhs_in

551553 case b of

552554 True -> tclift $ tfail (At fc

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

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

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

581583

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

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

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

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

586− probs <- get_probs

587− inj <- get_inj

588− return (res, probs, inj))

589−

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

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

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

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

588+ probs <- get_probs

589+ inj <- get_inj

590+ return (res, probs, inj))

591+ setContext ctxt'

592+ processTacticDecls newDecls

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

591594

592595 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

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

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

655658 logLvl 5 "STARTING CHECK"

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

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

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

658661 (do pbinds ist lhs_tm

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

660663 setNextName

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

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

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

665+ errAt "right hand side of " fname

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

663667 errAt "right hand side of " fname

664668 (erun fc $ psolve lhs_tm)

665669 hs <- get_holes

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

668672 tt <- get_term

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

670674 probs <- get_probs

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

672−

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

676+ setContext ctxt'

677+ processTacticDecls newDecls

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

674679

675680 logLvl 5 "DONE CHECK"

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

812817 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

824+ setContext ctxt'

825+ processTacticDecls newDecls

819826 let lhs_tm = orderPats (getInferTerm lhs')

820827 let lhs_ty = getInferType lhs'

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

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

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

829836 -- Elaborate wval in this context

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

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

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

832839 (bindTyArgs PVTy bargs infP) initEState

833840 (do pbinds i lhs_tm

834841 setNextName

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

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

838845 erun fc $ psolve lhs_tm

839846 tt <- get_term

840− return (tt, d, is))

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

848+ setContext ctxt'

849+ processTacticDecls newDecls

841850 def' <- checkDef fc defer

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

843852 addDeferred def''

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

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

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

925934 i <- getIState

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

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

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

928937 (do pbinds i lhs_tm

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

931940 psolve lhs_tm

932941 tt <- get_term

933− return (tt, d, is))

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

943+ setContext ctxt'

944+ processTacticDecls newDecls

945+

934946 def' <- checkDef fc defer

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

936948 addDeferred def''

src/Idris/Elab/Data.hs+2−1

@@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

215215 Idris (Name, Type)

216216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217217 = do checkUndefined fc n

218+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

218219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219220 ctxt <- getContext

220221 let cty' = normalise ctxt [] cty

@@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

223224 -- Check that the constructor type is, in fact, a part of the family being defined

224225 tyIs n cty'

225226

226− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

227+ logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

227228 logLvl 5 $ "Inaccessible args: " ++ show inacc

228229 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229230

src/Idris/Elab/Instance.hs+24−12

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

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

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

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

7979 (class_instances ci)

8080 addInstance intInst n iname

8181 Just _ -> addInstance intInst n iname

@@ -167,33 +167,45 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

167167 = do ty' <- addUsingConstraints syn fc t

168168 -- TODO think: something more in info?

169169 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

170+ let ty = addImpl [] i ty'

171171 ctxt <- getContext

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

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

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

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

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

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

175+ setContext ctxt'

176+ processTacticDecls newDecls

175177 ctxt <- getContext

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

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

179181

180− findOverlapping i t n

182+ findOverlapping i dets t n

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

182184 | otherwise

183185 = case lookupTy n (tt_ctxt i) of

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

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

186− case matchClause i tret' tret of

187− Right ms -> Just tret'

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

189− Right ms -> Just tret'

190− Left _ -> Nothing

188+ case matchArgs i dets tret' tret of

189+ Right _ -> Just tret'

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

191+ Right _ -> Just tret'

192+ Left _ -> Nothing

191193 _ -> Nothing

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

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

194196 getRetType (PPi _ _ _ sc) = getRetType sc

195197 getRetType t = t

196198

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+

197209 mkMethApp (n, _, _, ty)

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

199211 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

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

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

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

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

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

5959 (infTerm lhs)))

60+ setContext ctxt'

61+ processTacticDecls newDecls

6062 let lhs_tm = orderPats (getInferTerm lhs')

6163 let lhs_ty = getInferType lhs'

6264 let newargs = pvars i lhs_tm

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

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

6769

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

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

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

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

7173 (do pbinds i lhs_tm

7274 setNextName

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

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

7476 erun fc $ psolve lhs_tm

7577 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+

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

7884 let crhs_tm = renamepats pnames crhs_tm_in

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

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

@@ -57,17 +57,19 @@ buildType info syn fc opts n ty' = do

5757 ctxt <- getContext

5858 i <- getIState

5959

60− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

60+ logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

6161 ty' <- addUsingConstraints syn fc ty'

6262 ty' <- addUsingImpls syn n fc ty'

63− let ty = addImpl i ty'

63+ let ty = addImpl (imp_methods syn) i ty'

6464

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

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

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

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

6767

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

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

70− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

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

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

70+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

71+ setContext ctxt'

72+ processTacticDecls newDecls

7173

7274 let tyT = patToImp tyT'

7375

@@ -114,12 +116,14 @@ buildType info syn fc opts n ty' = do

114116 param_pos i ns t = []

115117

116118-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

118− FC -> FnOpts -> Name -> PTerm -> Idris Type

119+elabType :: ElabInfo -> SyntaxInfo

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

121+ -> FC -> FnOpts -> Name -> PTerm -> Idris Type

119122elabType = elabType' False

120123

121124elabType' :: Bool -> -- normalise it

122− ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

125+ ElabInfo -> SyntaxInfo ->

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

123127 FC -> FnOpts -> Name -> PTerm -> Idris Type

124128elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125129 n = liftname info n_in in -}

src/Idris/Elab/Utils.hs+10−8

@@ -22,7 +22,7 @@ import Debug.Trace

2222

2323import qualified Data.Map as Map

2424

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

2626

2727recheckC_borrowing uniq_check bs fc env t

2828 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

@@ -34,9 +34,13 @@ recheckC_borrowing uniq_check bs fc env t

3434 addConstraints fc cs

3535 return (tm, ty)

3636

37−

37+checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]

38+ -> Idris [(Name, (Int, Maybe Name, Type))]

3839checkDef fc ns = checkAddDef False True fc ns

3940

41+checkAddDef :: Bool -> Bool -> FC

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

43+ -> Idris [(Name, (Int, Maybe Name, Type))]

4044checkAddDef add toplvl fc [] = return []

4145checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

4246 = do ctxt <- getContext

@@ -46,7 +50,7 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

4650 ns' <- checkAddDef add toplvl fc ns

4751 return ((n, (i, top, t')) : ns')

4852

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

5054-- type

5155inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

5256inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

@@ -54,7 +58,7 @@ inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

5458 | otherwise = inaccessibleImps (i + 1) sc ins

5559inaccessibleImps _ _ _ = []

5660

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.

5862inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

5963inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

6064 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

@@ -74,10 +78,9 @@ elabCaseBlock info opts d@(PClauses f o n ps)

7478 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

7579 rec_elabDecl info EAll info (PClauses f opts' n ps )

7680

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

7882-- (i.e. - if we inferred any arguments that the user provided, make sure

7983-- they are the same!)

80−

8184checkInferred :: FC -> PTerm -> PTerm -> Idris ()

8285checkInferred fc inf user =

8386 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

@@ -92,9 +95,8 @@ checkInferred fc inf user =

9295 logLvl 10 $ "Checked match"

9396-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

9497

95−-- Return whether inferred term is different from given term

98+-- | Return whether inferred term is different from given term

9699-- (as above, but return a Bool)

97−

98100inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

99101inferredDiff fc inf user =

100102 do i <- getIState

src/Idris/Elab/Value.hs+9−4

@@ -56,16 +56,21 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam

5656elabValBind info aspat norm tm_in

5757 = do ctxt <- getContext

5858 i <- getIState

59− let tm = addImpl i tm_in

59+ let tm = addImpl [] i tm_in

6060 logLvl 10 (showTmImpls tm)

6161 -- try:

6262 -- * ordinary elaboration

6363 -- * elaboration as a Type

6464 -- * elaboration as a function a -> b

6565

66− ((tm', defer, is), _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP initEState

68− (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

66+ (ElabResult tm' defer is ctxt' newDecls, _) <-

67+ tclift (elaborate ctxt (sMN 0 "val") infP initEState

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+

6974 let vtm = orderPats (getInferTerm tm')

7075

7176 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

229229 ninfo = case namespace info of

230230 Nothing -> info { namespace = Just [n] }

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

233233 | what /= EDefns

234234 = 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

236236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237237 = do iLOG $ "Elaborating instance " ++ show n

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

1818import Idris.ErrReverse (errReverse)

1919import Idris.ElabQuasiquote (extractUnquotes)

2020import Idris.Elab.Utils

21+import Idris.Reflection

2122import qualified Util.Pretty as U

2223

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

@@ -36,6 +37,32 @@ import Debug.Trace

3637data ElabMode = ETyDecl | ELHS | ERHS

3738 deriving Eq

3839

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+

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

4067-- elaborated, typechecked term.

4168--

@@ -45,7 +72,7 @@ data ElabMode = ETyDecl | ELHS | ERHS

4572-- Also find deferred names in the term and their types

4673

4774build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

48− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

75+ ElabD ElabResult

4976build ist info emode opts fn tm

5077 = do elab ist info emode opts fn tm

5178 let tmIn = tm

@@ -64,7 +91,7 @@ build ist info emode opts fn tm

6491 mapM_ (\n -> when (n `elem` hs) $

6592 do focus n

6693 g <- goal

67− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

6895 (movelast n)) ivs

6996 ivs <- get_instances

7097 hs <- get_holes

@@ -72,7 +99,8 @@ build ist info emode opts fn tm

7299 mapM_ (\n -> when (n `elem` hs) $

73100 do focus n

74101 g <- goal

75− resolveTC True 7 g fn ist) ivs

102+ ptm <- get_term

103+ resolveTC True True 7 g fn ist) ivs

76104 tm <- get_term

77105 ctxt <- get_context

78106 probs <- get_probs

@@ -94,12 +122,13 @@ build ist info emode opts fn tm

94122 when tydecl (do update_term orderPats

95123 mkPat)

96124-- update_term liftPats)

97− EState is _ <- getAux

125+ EState is _ impls <- getAux

98126 tt <- get_term

99127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

100128 log <- getLog

101− if (log /= "") then trace log $ return (tm, ds, is)

102− else return (tm, ds, is)

129+ ctxt <- get_context

130+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

131+ else return (ElabResult tm ds is ctxt impls)

103132 where pattern = emode == ELHS

104133 tydecl = emode == ETyDecl

105134

@@ -114,7 +143,7 @@ build ist info emode opts fn tm

114143-- know about yet on the LHS of a pattern def)

115144

116145buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

117− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

146+ ElabD ElabResult

118147buildTC ist info emode opts fn tm

119148 = do -- set name supply to begin after highest index in tm

120149 let ns = allNamesIn tm

@@ -135,12 +164,13 @@ buildTC ist info emode opts fn tm

135164 -- unification

136165 when (not (null dots)) $

137166 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

167+ EState is _ impls <- getAux

139168 tt <- get_term

140169 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

141170 log <- getLog

142− if (log /= "") then trace log $ return (tm, ds, is)

143− else return (tm, ds, is)

171+ ctxt <- get_context

172+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

173+ else return (ElabResult tm ds is ctxt impls)

144174 where pattern = emode == ELHS

145175

146176-- return whether arguments of the given constructor name can be

@@ -183,9 +213,9 @@ goal_polymorphic =

183213 _ -> return True

184214 _ -> return False

185215

186−-- Returns the set of declarations we need to add to complete the definition

187−-- (most likely case blocks to elaborate)

188−

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

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

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

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

190220 ElabD ()

191221elab ist info emode opts fn tm

@@ -321,7 +351,7 @@ elab ist info emode opts fn tm

321351 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322352 _ -> elab' ina (Just fc) (PRef fc unitCon)

323353 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

325355 elab' ina fc (PResolveTC fc')

326356 = do c <- getNameFrom (sMN 0 "class")

327357 instanceArg c

@@ -540,7 +570,7 @@ elab ist info emode opts fn tm

540570 g <- goal

541571 hs <- get_holes

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

544574 (movelast n)

545575 else movelast n)

546576 (ivs' \\ ivs)

@@ -700,7 +730,7 @@ elab ist info emode opts fn tm

700730 env <- get_env

701731 hs <- get_holes

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

704734 (movelast n)

705735 else movelast n)

706736 (ivs' \\ ivs)

@@ -965,17 +995,14 @@ elab ist info emode opts fn tm

965995 elab' ina fc (PUnifyLog t) = do unifyLog True

966996 elab' ina fc t

967997 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

969999 = do -- First extract the unquoted subterms, replacing them with fresh

9701000 -- names in the quasiquoted term. Claim their reflections to be

9711001 -- an inferred type (to support polytypic quasiquotes).

1002+ finalTy <- goal

9721003 (t, unq) <- extractUnquotes 0 t

9731004 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

978−

1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames

9791006

9801007 -- Save the old state - we need a fresh proof state to avoid

9811008 -- capturing lexically available variables in the quoted term.

@@ -1010,7 +1037,7 @@ elab ist info emode opts fn tm

10101037 letbind nTm (Var qTy) (Var qTm)

10111038

10121039 -- Fill out the goal type, if relevant

1013− case goal of

1040+ case goalt of

10141041 Nothing -> return ()

10151042 Just gTy -> do focus qTy

10161043 elabE (ina { e_qq = True }) fc gTy

@@ -1025,18 +1052,20 @@ elab ist info emode opts fn tm

10251052 env <- get_env

10261053 loadState

10271054 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

10291058 case quoted of

10301059 Just q -> do ctxt <- get_context

10311060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

10321061 if pattern

1033− then do try' (reflectTTQuotePattern unquoteNames q')

1034− (reflectRawQuotePattern unquoteNames (forget q'))

1035− True

1036− else do try' (fill $ reflectTTQuote unquoteNames q')

1037− -- we forget q' instead of using q to ensure rechecking

1038− (fill $ reflectRawQuote unquoteNames (forget q'))

1039− True -- ignore errors like proof search does

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1064+ else reflectTTQuotePattern unquoteNames q'

1065+ else do if isRaw

1066+ then -- we forget q' instead of using q to ensure rechecking

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1068+ else fill $ reflectTTQuote unquoteNames q'

10401069 solve

10411070

10421071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

@@ -1077,8 +1106,8 @@ elab ist info emode opts fn tm

10771106 focus n

10781107 elab' ina (Just fc') tm

10791108 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

10821111 solve

10831112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

10841113

@@ -1346,7 +1375,7 @@ findInstances :: IState -> Term -> [Name]

13461375findInstances ist t

13471376 | (P _ n _, _) <- unApply t

13481377 = case lookupCtxt n (idris_classes ist) of

1349− [CI _ _ _ _ _ ins] -> ins

1378+ [CI _ _ _ _ _ ins _] -> ins

13501379 _ -> []

13511380 | otherwise = []

13521381

@@ -1376,14 +1405,26 @@ proofSearch' ist rec ambigok depth prv top n hints

13761405-- Resolve type classes. This will only pick up 'normal' instances, never

13771406-- named instances (hence using 'tcname' to check it's a generated instance

13781407-- name).

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1380−resolveTC = resTC' []

1381−

1382−resTC' tcs def 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

1384−resTC' tcs defaultOn depth topg fn ist

1385− = do compute

1386− g <- goal

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

1413+ -> IState -> ElabD ()

1414+resolveTC def mvok depth top fn ist

1415+ = do hs <- get_holes

1416+ resTC' [] def hs depth top fn ist

1417+

1418+resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1419+resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1420+resTC' tcs defaultOn topholes depth topg fn ist

1421+ = do compute

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

13871428 ptm <- get_term

13881429 ulog <- getUnifyLog

13891430 hs <- get_holes

@@ -1400,6 +1441,31 @@ resTC' tcs defaultOn depth topg fn ist

14001441 let depth' = if scopeOnly then 2 else depth

14011442 blunderbuss t depth' stk (stk ++ insts)) True

14021443 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+

14031469 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

14041470 | otherwise = (fail "Can't resolve", show n)

14051471

@@ -1427,10 +1493,13 @@ resTC' tcs defaultOn depth topg fn ist

14271493

14281494 blunderbuss t d stk [] = do -- c <- get_env

14291495 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1496+ lift $ tfail $ CantResolve False topg

14311497 blunderbuss t d stk (n:ns)

14321498 | n /= fn && (n `elem` stk || tcname n)

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1499+ = tryCatch (resolve n d)

1500+ (\e -> case e of

1501+ CantResolve True _ -> lift $ tfail e

1502+ _ -> blunderbuss t d stk ns)

14341503 | otherwise = blunderbuss t d stk ns

14351504

14361505 resolve n depth

@@ -1459,7 +1528,7 @@ resTC' tcs defaultOn depth topg fn ist

14591528 let got = fst (unApply t)

14601529 let depth' = if tc' `elem` tcs

14611530 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1531+ resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

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

14641533 -- if there's any arguments left, we've failed to resolve

14651534 hs <- get_holes

@@ -1505,11 +1574,17 @@ case_ ind autoSolve ist fn tm = do

15051574 else casetac (forget val)

15061575 when autoSolve solveAll

15071576

1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1577+tacN :: String -> Name

1578+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1579+

1580+runTactical :: FC -> Env -> Term -> ElabD ()

1581+runTactical fc env tm = do tm' <- eval tm

1582+ runTacTm tm'

1583+ return ()

15101584 where

1511− eval = normaliseAll ctxt env . finalise

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

1585+ eval tm = do ctxt <- get_context

1586+ return $ normaliseAll ctxt env (finalise tm)

1587+

15131588 returnUnit = fmap fst $ get_type_val (Var unitCon)

15141589

15151590 -- | 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 ()

15471622 = do env <- get_env

15481623 fmap fst . get_type_val $ reflectEnv env

15491624 | n == tacN "prim__Fail", [_a, errs] <- args

1550− = do parts <- reifyReportParts (eval errs)

1625+ = do errs' <- eval errs

1626+ parts <- reifyReportParts errs'

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

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

15531629 = return tm

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

1555− = do let first' = eval first

1631+ = do first' <- eval first

15561632 res <- runTacTm first'

1557− let next = eval (App andThen res)

1633+ next <- eval (App andThen res)

15581634 runTacTm next

15591635 | n == tacN "prim__Try", [_a, first, alt] <- args

1560− = do let first' = eval first

1561− let alt' = eval alt

1636+ = do first' <- eval first

1637+ alt' <- eval alt

15621638 try' (runTacTm first') (runTacTm alt') True

15631639 | n == tacN "prim__Fill", [raw] <- args

15641640 = do raw' <- reifyRaw raw

15651641 apply raw' []

15661642 returnUnit

1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

1568− = do n <- getNameFrom (sMN 0 hint)

1569− fmap fst $ get_type_val (reflectName n)

1643+ | n == tacN "prim__Gensym", [hint] <- args

1644+ = do hintStr <- eval hint

1645+ case hintStr of

1646+ Constant (Str h) -> do

1647+ n <- getNameFrom (sMN 0 h)

1648+ fmap fst $ get_type_val (reflectName n)

1649+ _ -> fail "no hint"

15701650 | n == tacN "prim__Claim", [n, ty] <- args

15711651 = do n' <- reifyTTName n

15721652 ty' <- reifyRaw ty

@@ -1596,6 +1676,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15961676 Just name -> fmap Just $ reifyTTName name

15971677 intro n

15981678 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

15991702 | n == tacN "prim__Debug", [ty, msg] <- args

16001703 = do let msg' = fromTTMaybe msg

16011704 case msg' of

@@ -1850,6 +1953,7 @@ runTac autoSolve ist perhapsFC fn tac

18501953 Just fc ->

18511954 do fill $ reflectFC fc

18521955 solve

1956+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

18531957 runT x = fail $ "Not implemented " ++ show x

18541958

18551959 runReflected t = do t' <- reify ist t

@@ -2361,7 +2465,7 @@ reflectTTQuote unq (P nt n t)

23612465reflectTTQuote unq (V n)

23622466 = reflCall "V" [RConstant (I n)]

23632467reflectTTQuote 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]

23652469reflectTTQuote unq (App f x)

23662470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

23672471reflectTTQuote unq (Constant c)

@@ -2378,7 +2482,7 @@ reflectRawQuote unq (Var n)

23782482 | n `elem` unq = Var n

23792483 | otherwise = reflCall "Var" [reflectName n]

23802484reflectRawQuote 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]

23822486reflectRawQuote unq (RApp f x) =

23832487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

23842488reflectRawQuote unq RType = Var (reflm "RType")

@@ -2436,27 +2540,27 @@ reflectNameQuotePattern _ -- for all other names, match any

24362540 solve

24372541

24382542reflectBinder :: Binder Term -> Raw

2439−reflectBinder = reflectBinderQuote reflectTTQuote []

2440−

2441−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2442−reflectBinderQuote q unq (Lam t)

2443− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2444−reflectBinderQuote q unq (Pi _ t k)

2445− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2446−reflectBinderQuote q unq (Let x y)

2447− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2448−reflectBinderQuote q unq (NLet x y)

2449− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2450−reflectBinderQuote q unq (Hole t)

2451− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2452−reflectBinderQuote q unq (GHole _ t)

2453− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2454−reflectBinderQuote q unq (Guess x y)

2455− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2456−reflectBinderQuote q unq (PVar t)

2457− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2458−reflectBinderQuote q unq (PVTy t)

2459− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2543+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2544+

2545+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2546+reflectBinderQuote q ty unq (Lam t)

2547+ = reflCall "Lam" [Var ty, q unq t]

2548+reflectBinderQuote q ty unq (Pi _ t k)

2549+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2550+reflectBinderQuote q ty unq (Let x y)

2551+ = reflCall "Let" [Var ty, q unq x, q unq y]

2552+reflectBinderQuote q ty unq (NLet x y)

2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2554+reflectBinderQuote q ty unq (Hole t)

2555+ = reflCall "Hole" [Var ty, q unq t]

2556+reflectBinderQuote q ty unq (GHole _ t)

2557+ = reflCall "GHole" [Var ty, q unq t]

2558+reflectBinderQuote q ty unq (Guess x y)

2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2560+reflectBinderQuote q ty unq (PVar t)

2561+ = reflCall "PVar" [Var ty, q unq t]

2562+reflectBinderQuote q ty unq (PVTy t)

2563+ = reflCall "PVTy" [Var ty, q unq t]

24602564

24612565mkList :: Raw -> [Raw] -> Raw

24622566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2603,11 +2707,14 @@ reflectErr (NotInjective t1 t2 t3) =

26032707 , reflect t2

26042708 , reflect t3

26052709 ]

2606−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2710+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

26072711reflectErr (CantResolveAlts ss) =

26082712 raw_apply (Var $ reflErrName "CantResolveAlts")

26092713 [rawList (Var $ reflm "TTName") (map reflectName ss)]

26102714reflectErr (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]

26112718reflectErr UniverseError = Var $ reflErrName "UniverseError"

26122719reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

26132720reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2748,6 +2855,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

27482855 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

27492856reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

27502857

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+

27512880envTupleType :: Raw

27522881envTupleType

27532882 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/IBC.hs+12−8

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

@@ -365,7 +365,7 @@ pClasses cs = mapM_ (\ (n, c) ->

365365 -- Don't lose instances from previous IBCs, which

366366 -- could have loaded in any order

367367 let is = case lookupCtxtExact n (idris_classes i) of

368− Just (CI _ _ _ _ _ ins) -> ins

368+ Just (CI _ _ _ _ _ ins _) -> ins

369369 _ -> []

370370 let c' = c { class_instances =

371371 class_instances c ++ is }

@@ -1238,7 +1238,7 @@ instance (Binary t) => Binary (PDecl' t) where

12381238 put x7

12391239 put x8

12401240 put x9

1241− PClass x1 x2 x3 x4 x5 x6 x7 x8

1241+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

12421242 -> do putWord8 7

12431243 put x1

12441244 put x2

@@ -1248,6 +1248,7 @@ instance (Binary t) => Binary (PDecl' t) where

12481248 put x6

12491249 put x7

12501250 put x8

1251+ put x9

12511252 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

12521253 do putWord8 8

12531254 put x1

@@ -1346,7 +1347,8 @@ instance (Binary t) => Binary (PDecl' t) where

13461347 x6 <- get

13471348 x7 <- get

13481349 x8 <- get

1349− return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1350+ x9 <- get

1351+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

13501352 8 -> do x1 <- get

13511353 x2 <- get

13521354 x3 <- get

@@ -1418,7 +1420,7 @@ instance Binary Using where

14181420 _ -> error "Corrupted binary data for Using"

14191421

14201422instance Binary SyntaxInfo where

1421− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1423+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

14221424 = do put x1

14231425 put x2

14241426 put x3

@@ -1434,7 +1436,7 @@ instance Binary SyntaxInfo where

14341436 x5 <- get

14351437 x6 <- get

14361438 x7 <- get

1437− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)

1439+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

14381440

14391441instance (Binary t) => Binary (PClause' t) where

14401442 put x

@@ -2071,19 +2073,21 @@ instance (Binary t) => Binary (PArg' t) where

20712073

20722074

20732075instance Binary ClassInfo where

2074− put (CI x1 x2 x3 x4 x5 _)

2076+ put (CI x1 x2 x3 x4 x5 _ x6)

20752077 = do put x1

20762078 put x2

20772079 put x3

20782080 put x4

20792081 put x5

2082+ put x6

20802083 get

20812084 = do x1 <- get

20822085 x2 <- get

20832086 x3 <- get

20842087 x4 <- get

20852088 x5 <- get

2086− return (CI x1 x2 x3 x4 x5 [])

2089+ x6 <- get

2090+ return (CI x1 x2 x3 x4 x5 [] x6)

20872091

20882092instance Binary OptInfo where

20892093 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

@@ -585,8 +585,8 @@ collect (c@(PClauses _ o _ _) : ds)

585585collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

586586collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588−collect (PClass doc f s cs n ps pdocs ds : ds')

589− = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

588+collect (PClass doc f s cs n ps pdocs fds ds : ds')

589+ = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

590590collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591591 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592592collect (d : ds) = d : collect ds

src/Idris/Parser.hs+5−1

@@ -612,11 +612,15 @@ class_ syn = do (doc, argDocs, acc)

612612 n_in <- fnName

613613 let n = expandNS syn n_in

614614 cs <- many carg

615+ fds <- option (map fst cs) fundeps

615616 ds <- option [] (classBlock syn)

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

618619 <?> "type-class declaration"

619620 where

621+ fundeps :: IdrisParser [Name]

622+ fundeps = do lchar '|'; sepBy name (lchar ',')

623+

620624 carg :: IdrisParser (Name, PTerm)

621625 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

622626 return (i, ty)

src/Idris/REPL.hs+1−1

@@ -773,7 +773,7 @@ process fn (NewDefn decls) = do

773773 getName (PTy docs argdocs syn fc opts name ty) = Just name

774774 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

775775 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

777777 getName _ = Nothing

778778 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

779779 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

src/Idris/TypeSearch.hs+1−1

@@ -46,7 +46,7 @@ searchByType pkgs pterm = do

4646 mapM_ loadPkgIndex pkgs

4747 pterm' <- addUsingConstraints syn emptyFC pterm

4848 pterm'' <- implicit toplevel syn name pterm'

49− let pterm''' = addImpl i pterm''

49+ let pterm''' = addImpl [] i pterm''

5050 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

5151 let names = searchUsing searchPred i ty

5252 let names' = take numLimit names

test/basic002/test006.idr+1−1

@@ -18,7 +18,7 @@ natToBin k with (parity k)

1818 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

1919

2020main : IO ()

21−main = do print (natToBin 42)

21+main = do printLn (natToBin 42)

2222

2323---------- Proofs ----------

2424

test/basic003/test027.idr+3−3

@@ -19,7 +19,7 @@ using (Ord a, Num n)

1919 mprod (x :: xs) = x * mprod xs

2020

2121main : IO ()

22−main = do print $ isort [1,5,3,5,1,9,8]

23− print $ msum [1..10]

24− print $ mprod [1..10]

22+main = do printLn $ isort [1,5,3,5,1,9,8]

23+ printLn $ msum [1..10]

24+ printLn $ mprod [1..10]

2525

test/basic004/test016.idr+1−1

@@ -13,5 +13,5 @@ take (S n) (x :: xs) = x :: take n xs

1313take n [] = []

1414

1515main : IO ()

16−main = do print (take 10 (Main.countFrom 10))

16+main = do printLn (take 10 (Main.countFrom 10))

1717

test/basic005/test019.lidr+1−1

@@ -14,5 +14,5 @@

1414> | False = ifFalse x

1515

1616> main : IO ()

17−> main = print (test ((S 4) ==) 5 Oh)

17+> main = printLn (test ((S 4) ==) 5 Oh)

1818

test/basic006/test020.idr+2−2

@@ -21,7 +21,7 @@ test : Integer -> String

2121test x = "Number " ++ x

2222

2323main : IO ()

24−main = do print (foo [1,2,3])

25− print (test 42)

24+main = do printLn (foo [1,2,3])

25+ printLn (test 42)

2626

2727

test/basic006/test020a.idr+1−1

@@ -16,5 +16,5 @@ foo : Vect n a -> List a

1616foo xs = reverse xs

1717

1818main : IO ()

19−main = print (foo [1,2,3])

19+main = printLn (foo [1,2,3])

2020

test/basic007/test033.idr+1−1

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

11module Main

22

33main : IO ()

4−main = nullPtr null >>= print

4+main = nullPtr null >>= printLn

test/basic011/basic011.idr+10−10

@@ -3,14 +3,14 @@ module Main

33import Data.Hash

44

55main : IO ()

6−main = do print $ hash (the Bits8 3)

7− print $ hash (the (List Bits8) [3])

8− print $ hash "hello world"

9− print $ hash 'a'

10− print $ hash (the Bits8 3)

11− print $ hash (the Bits16 3)

12− print $ hash (the Bits32 3)

13− print $ hash (the Bits64 3)

14− print $ hash (the Int 3)

15− print $ hash (the Integer 3)

6+main = do printLn $ hash (the Bits8 3)

7+ printLn $ hash (the (List Bits8) [3])

8+ printLn $ hash "hello world"

9+ printLn $ hash 'a'

10+ printLn $ hash (the Bits8 3)

11+ printLn $ hash (the Bits16 3)

12+ printLn $ hash (the Bits32 3)

13+ printLn $ hash (the Bits64 3)

14+ printLn $ hash (the Int 3)

15+ printLn $ hash (the Integer 3)

1616

test/basic012/basic012.idr+5−4

@@ -1,7 +1,7 @@

11import Data.Vect

22import Control.Monad.State

33import Control.Monad.Identity

4−

4+

55VThing : Type

66VThing = {n : Nat} -> Vect n Int -> Int

77

@@ -31,7 +31,8 @@ testfoo3 xs = foo 42 xs (bar 10)

3131AnyST : Type -> Type -> Type

3232AnyST s a = {m : _} -> Monad m => StateT s m a

3333

34−foost: AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

3536foost = do x <- get

3637 put x

3738

@@ -52,11 +53,11 @@ tupleId f (a, b) = (f a, f b)

5253

5354AppendType : Type

5455AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55−

56+

5657append : AppendType

5758append [] ys = ys

5859append (x :: xs) ys = x :: append xs ys

5960

6061main : IO ()

6162main = 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]

9696testEnv x = [x,x]

9797

9898main : IO ()

99−main = do { print testFac

100− print test }

99+main = do { printLn testFac

100+ printLn test }

101101

102102

103103

test/effects002/test025.idr+1−1

@@ -30,6 +30,6 @@ testMemory = do Src :- allocate 5

3030

3131main : IO ()

3232main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

33− (\err => print err) (\ok => print ok)

33+ (\err => printLn err) (\ok => printLn ok)

3434

3535

test/io002/test008.idr+1−1

@@ -22,7 +22,7 @@ main = do (a, b) <- ioVals

2222 let x = "bar"

2323 putStrLn (show (getVal x 7 testlist))

2424 let ((y, z) :: _) = testlist

25− print z

25+ printLn z

2626 case lookup x testlist of

2727 Just v => putStrLn (show v)

2828 Nothing => putStrLn "Not there!"

test/io003/test018a.idr+1−1

@@ -27,7 +27,7 @@ mainProc = do mainID <- myID

2727

2828repeatIO : Int -> IO ()

2929repeatIO 0 = return ()

30−repeatIO n = do print n

30+repeatIO n = do printLn n

3131 run mainProc

3232 repeatIO (n - 1)

3333

test/primitives001/test005.idr+6−6

@@ -7,9 +7,9 @@ tlist : List Int

77tlist = [1, 2, 3, 4, 5]

88

99main : IO ()

10−main = do print (abs (-8))

11− print (abs (S Z))

12− print (span isAlpha tstr)

13− print (break isDigit tstr)

14− print (span (\x => x < 3) tlist)

15− print (break (\x => x > 2) tlist)

10+main = do printLn (abs (-8))

11+ printLn (abs (S Z))

12+ printLn (span isAlpha tstr)

13+ printLn (break isDigit tstr)

14+ printLn (span (\x => x < 3) tlist)

15+ printLn (break (\x => x > 2) tlist)

test/proof003/test015.idr+3−3

@@ -72,10 +72,10 @@ readNum = do putStr "Enter a number:"

7272

7373main : IO ()

7474main = do let Just bin1 = natToBin 8 42

75− print bin1

75+ printLn bin1

7676 let Just bin2 = natToBin 8 89

77− print bin2

78− print (adc bin1 bin2 b0)

77+ printLn bin2

78+ printLn (adc bin1 bin2 b0)

7979

8080

8181

test/records001/test011.idr+5−5

@@ -20,9 +20,9 @@ person = MkPerson "Fred" 30

2020main : IO ()

2121main = do let x = record { name = "foo",

2222 more_things = reverse ["a","b"] } testFoo

23− print $ name x

24− print $ name person

25− print $ things x

26− print $ more_things x

27− print $ age (record { age = 25 } person)

23+ printLn $ name x

24+ printLn $ name person

25+ printLn $ things x

26+ printLn $ more_things x

27+ printLn $ age (record { age = 25 } person)

2828

test/records003/records003.idr+6−6

@@ -38,10 +38,10 @@ test : Meeting 2015

3838test = next_year idm_gbg

3939

4040main : IO ()

41−main = do print (record { event->organiser->name } test)

42− print (record { event->organiser->age } test)

43− print (record { event->organiser->age } idm_gbg)

44− print (record { organiser->age } test)

45− print (record { organiser->age } idm_gbg)

46− print (record { year } idm_gbg)

41+main = do printLn (record { event->organiser->name } test)

42+ printLn (record { event->organiser->age } test)

43+ printLn (record { event->organiser->age } idm_gbg)

44+ printLn (record { organiser->age } test)

45+ printLn (record { organiser->age } idm_gbg)

46+ printLn (record { year } idm_gbg)

4747

test/reg002/reg012.idr+1−1

@@ -30,4 +30,4 @@ swap (x :: Nil) = x :: Nil

3030swap (x :: y :: xs) = (y :: x :: (swap xs))

3131

3232main : 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

1313 r2 = r

1414

1515main : 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

22

33main : IO ()

44main = do

5− print $ prim_lenString "hallo"

6− print $ prim_lenString "1"

7− print $ prim_lenString ""

5+ printLn $ prim_lenString "hallo"

6+ printLn $ prim_lenString "1"

7+ printLn $ prim_lenString ""

88

test/reg016/reg016.idr+6−6

@@ -1,11 +1,11 @@

11module Main

22

33main : IO ()

4−main = do print $ the Integer 429496729500000000000000

5−-- print $ the Integer 4294967296

6−-- print $ the Integer 4294967297

7−-- print $ the Int 4294967295

8−-- print $ the Int 4294967296

9−-- print $ the Int 4294967297

4+main = do printLn $ the Integer 429496729500000000000000

5+-- printLn $ the Integer 4294967296

6+-- printLn $ the Integer 4294967297

7+-- printLn $ the Int 4294967295

8+-- printLn $ the Int 4294967296

9+-- printLn $ the Int 4294967297

1010

1111

test/reg017/reg017.idr+1−1

@@ -10,4 +10,4 @@ foo : { t : Type } ->

1010foo {t} a {prfA = p} b c {prfBC} = b

1111

1212main : 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) =

1212 (v, x::vs)

1313

1414main : 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

2727 \x => show val

2828

2929main : IO ()

30−main = do print dbl

30+main = do printLn dbl

3131 putStrLn (foo 3)

3232

test/reg029/reg029.idr+2−2

@@ -7,5 +7,5 @@ import System

77

88main : IO ()

99main = do

10− print !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11− print !(getEnv "IDRIS_REG029_EXISTENT_VAR")

10+ printLn !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11+ printLn !(getEnv "IDRIS_REG029_EXISTENT_VAR")

test/reg031/reg031.idr+1−1

@@ -1,7 +1,7 @@

11module Main

22

33main : 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"

55 where

66 -- make the values positive if the backend has signed chars

77 val : Char -> Int

test/reg040/reg040.idr+1−1

@@ -4,4 +4,4 @@ io : IO Int

44io = return 42

55

66main : 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

2121-- Here, we'd apply the not-a-function to the erased argument 4,

2222-- which would make the program go wrong.

2323main : 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

1515foo = (1 :: 2 :: 3 :: Nil)

1616

1717main : IO ()

18−main = print foo

18+main = printLn foo

1919

test/reg052/reg052.idr+1−1

@@ -5,4 +5,4 @@ impure_int : IO Int

55impure_int = return 41

66

77main : IO ()

8−main = impure_int >>= impure_op . prim__zextInt_B64 >>= print

8+main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/reg059/expectednew file

No changes to the content.

test/reg059/reg059.idrnew file+8

@@ -0,0 +1,8 @@

1+class Monad m => ContainerMonad (m : Type -> Type) where

2+ Elem : a -> m a -> Type

3+ tagElem : (mx : m a) -> m (x : a ** Elem x mx)

4+

5+class Monad m => ContainerMonad2 a (m : Type -> Type) where

6+ Elem2 : a -> m a -> Type

7+ tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

8+

test/reg059/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg059.idr --check

3+rm -f *.ibc

test/sourceLocation001/SourceLoc.idr+4−4

@@ -36,7 +36,7 @@ using (ctxt : Vect n Ty)

3636 Var : (i : Fin n) -> Tm ctxt (index i ctxt)

3737 Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

3838 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

4040 Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

4141

4242 data Env : Vect n Ty -> Type where

@@ -83,11 +83,11 @@ testTerm4 = App testTerm3 MkU

8383namespace Main

8484 main : IO ()

8585 main = do putStrLn "Testing using definition"

86− print fromRHS

86+ printLn fromRHS

8787 putStrLn "Testing using inline tactics"

88− print fromProofScript

88+ printLn fromProofScript

8989 putStrLn "Testing using metavariable with later definition"

90− print fromMetavar

90+ printLn fromMetavar

9191 putStrLn "-----------------------"

9292 sequence_ $ with List [ exec testTerm1

9393 , exec testTerm2

test/sugar001/test007.idr+4−4

@@ -35,7 +35,7 @@ runEval env e with (eval e) {

3535}

3636

3737main : IO ()

38−main = do print [| (\x => x *2) (Just 4) |]

39− print [| plus (Just 4) (Just 5) |]

40− print (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"))))

38+main = do printLn [| (\x => x *2) (Just 4) |]

39+ printLn [| plus (Just 4) (Just 5) |]

40+ printLn (runEval [("x",21), ("y", 20)] (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'

99main : IO ()

1010main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

1111 | (x :: y :: _) => putStrLn "Too many arguments!"

12− print (foo (Just (cast a)))

12+ printLn (foo (Just (cast a)))

1313

1414{-

1515

test/sugar005/As.idr+9−9

@@ -24,13 +24,13 @@ same _ _ = Nothing

2424

2525namespace Main

2626 main : IO ()

27− main = do print $ isS 0

28− print $ isS 1

29− print $ hasS [0,0,0]

30− print $ hasS [0,1,2]

31− print $ isSS 5

32− print $ isSS 0

33− print $ same 1 1

34− print $ same 0 0

35− print $ same 1 0

27+ main = do printLn $ isS 0

28+ printLn $ isS 1

29+ printLn $ hasS [0,0,0]

30+ printLn $ hasS [0,1,2]

31+ printLn $ isSS 5

32+ printLn $ isSS 0

33+ printLn $ same 1 1

34+ printLn $ same 0 0

35+ printLn $ same 1 0

3636

test/tactics001/Tactics.idr+14

@@ -2,6 +2,9 @@ module Tactics

22

33import Language.Reflection.Tactical

44

5+import Data.Vect

6+

7+

58%default total

69

710-- Test that basic proofs with new-style tactics work

@@ -25,3 +28,14 @@ plusSuccRightSuccNew (S j) k =

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

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

2730 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

2121countStream x = x :: countStream (x + 1)

2222

2323main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

2525

test/totality004/totality004a.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

2121countStream x = x :: countStream (x + 1)

2222

2323main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

2525

test/totality005/totality005.idr+1−1

@@ -7,4 +7,4 @@ fib : Stream Nat

77fib = 0 :: zipWithS (+) fib (1 :: fib)

88

99partial 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

3434main : IO ()

3535main = do putStr "Enter a number: "

3636 x <- getLine

37− print (natToBin (fromInteger (cast x)))

37+ printLn (natToBin (fromInteger (cast x)))

3838

3939---------- Proofs ----------

4040