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

CHANGELOG+8−1

compare with master

unifiedsplit

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

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

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

34 command :elaborate-term for serialized terms.

35−

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

36+ aligned, semantically.

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

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

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

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

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

42+ are checked when checking for overlapping instances.

36

43

37New in 0.9.16:

44New in 0.9.16:

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

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

Setup.hs+9−2

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

57 Just False -> False

58 Nothing -> True

59

60+execOnly :: S.ConfigFlags -> Bool

61+execOnly flags =

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

63+ Just True -> True

64+ Just False -> False

65+ Nothing -> True

66+

60isRelease :: S.ConfigFlags -> Bool

67isRelease :: S.ConfigFlags -> Bool

61isRelease flags =

68isRelease flags =

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

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

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

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

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

177 return (Just buildinfo, [])

184 return (Just buildinfo, [])

178

185

179−idrisBuild _ flags _ local = do

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

180 buildStdLib

187 buildStdLib

181 buildRTS

188 buildRTS

182 where

189 where

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

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

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

200-- Copy/Install

207-- Copy/Install

201

208

202−idrisInstall verbosity copy pkg local = do

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

203 installStdLib

210 installStdLib

204 installRTS

211 installRTS

205 where

212 where

benchmarks/quasigroups/Main.idr+2−2

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

14 Left err => putStrLn err

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

16 putStrLn "Got board:"

17− print board

17+ printLn board

18 putStrLn "Solving..."

19 case fillBoard board legal of

20 Nothing => putStrLn "No solution found"

21 Just (solved ** _) => do

22 putStrLn "Solution found:"

23− print solved

23+ printLn solved

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

benchmarks/trivial/sortvec.idr+2−3

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

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

14

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

16−mkSortVec Z = return []

16+mkSortVec Z = return []

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

18

19main : IO ()

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

21-- let arg = "2000"

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

23 putStrLn "Made vector"

24− print (vsort vec)

24+ printLn (vsort vec)

25−

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

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

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

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

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

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

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

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

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

13 exec_db_v2 stmt -- execute the prepared query

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

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

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

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

17 close_db db -- close the datbase

18 return ()

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

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

23 let x = (fst sql)

24 let list = (snd sql)

25− liftIO(print x)

25+ liftIO(printLn x)

26 stmt <- (prepare_db db x)

27 bindMulti stmt list

28 exec_db_v2 stmt

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

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

36 let x = (fst sql)

37 let list = (snd sql)

38− liftIO(print x)

38+ liftIO(printLn x)

39 stmt <- (prepare_db db x)

40 bindMulti stmt list

41 exec_db_v2 stmt

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

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

49 let x = (fst sql)

50 let list = (snd sql)

51− liftIO(print x)

51+ liftIO(printLn x)

52 stmt <- (prepare_db db x)

53 bindMulti stmt list

54 exec_db_v2 stmt

55 res <- toList_v1 db

56− liftIO(print res)

56+ liftIO(printLn res)

57 finalize_db stmt

58 close_db db

59 return ()

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

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

65 let x = (fst sql)

66 let list = (snd sql)

67− liftIO(print x)

67+ liftIO(printLn x)

68 stmt <- (prepare_db db x)

69 bindMulti stmt list

70 exec_db_v2 stmt

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

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

79 let x = (fst sql)

80 let list = (snd sql)

81− liftIO(print x)

81+ liftIO(printLn x)

82 stmt <- (prepare_db db x)

83 bindMulti stmt list

84 exec_db_v2 stmt

85 res <- toList_v1 db

86− liftIO(print res)

86+ liftIO(printLn res)

87 finalize_db stmt

88 close_db db

89 return ()

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

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

95 let x = (fst sql)

96 let list = (snd sql)

97− liftIO(print x)

97+ liftIO(printLn x)

98 stmt <- (prepare_db db x)

99 bindMulti stmt list

100 exec_db_v2 stmt

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

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

109 let x = (fst sql)

110 let list = (snd sql)

111− liftIO(print x)

111+ liftIO(printLn x)

112 stmt <- (prepare_db db x)

113 bindMulti stmt list

114 exec_db_v2 stmt

115 res <- toList_v1 db

116− liftIO(print res)

116+ liftIO(printLn res)

117 finalize_db stmt

118 close_db db

119 return ()

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

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

124 let x = (fst sql)

125 let list = (snd sql)

126− liftIO(print x)

126+ liftIO(printLn x)

127 stmt <- (prepare_db db x)

128 bindMulti stmt list

129 exec_db_v2 stmt

130 res <- toList_v1 db

131− liftIO(print res)

131+ liftIO(printLn res)

132 finalize_db stmt

133 close_db db

134 return ()

idris.cabal+9

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

293 test/reg058/run

294 test/reg058/*.idr

295 test/reg058/expected

296+ test/reg059/run

297+ test/reg059/*.idr

298+ test/reg059/expected

296

299

297 test/basic001/run

300 test/basic001/run

298 test/basic001/*.idr

301 test/basic001/*.idr

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

662 Default: False

665 Default: False

663 manual: True

666 manual: True

664

667

668+Flag execonly

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

670+ Default: False

671+ manual: True

672+

665Library

673Library

666 hs-source-dirs: src

674 hs-source-dirs: src

667 Exposed-modules:

675 Exposed-modules:

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

729 , Idris.ProofSearch

737 , Idris.ProofSearch

730 , Idris.Prover

738 , Idris.Prover

731 , Idris.Providers

739 , Idris.Providers

740+ , Idris.Reflection

732 , Idris.REPL

741 , Idris.REPL

733 , Idris.REPLParser

742 , Idris.REPLParser

734 , Idris.Transforms

743 , Idris.Transforms

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

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

6%access public

7

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

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

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

10 ||| Get the context

11 get : m s

12 ||| Write a new context/output

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

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

51

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

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

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

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

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

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

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

56 return (a, f' w)

57 return (a, f' w)

57

58

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

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

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

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

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

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

182+ , TermPart `(Integer : Type)

183 ]

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

185 = mkFinIntegerErr n m

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

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

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

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

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

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

275 show UniverseError = "UniverseError"

276 show UniverseError = "UniverseError"

276 show ProgramLineComment = "ProgramLineComment"

277 show ProgramLineComment = "ProgramLineComment"

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

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

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

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

146isEmptySizeZero Empty p = Refl

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

148

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

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

150emptyHeapValid = Refl

151

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

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

182 does seem to work correctly!

183main : IO ()

184main = do

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

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

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

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

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

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

188 return ()

189-}

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

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

36 eq (f a) (f b)

37

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

39−minimum x y with (order x y)

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

40 | Left _ = x

41 | Right _ = y

42

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

44−maximum x y with (order x y)

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

45 | Left _ = y

46 | Right _ = x

47

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

103decideLTE Z y = Yes LTEZero

104decideLTE (S x) Z = No zeroNeverGreater

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

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

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

107 | No _ with (decideLTE x y)

108 | Yes nLTEm = Yes (LTESucc nLTEm)

109 | No nGTm = No (ltesuccinjective nGTm)

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

122instance Ordered Nat LTE where

123 order Z n = Left LTEZero

124 order m Z = Right LTEZero

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

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

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

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

128

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

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

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

9

10instance Handler (Exception a) Maybe where

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

14 handle _ (Raise e) k = []

15

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

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

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

18 believe_me (exit 1)

19

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

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

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

39

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

41-- handler can be introduced mid interpretation?

42−

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

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

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

43putStr s = call $ PutStr s

44

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

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

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

48+

45||| Write a character to standard output.

49||| Write a character to standard output.

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

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

47putChar c = call $ PutCh c

51putChar c = call $ PutCh c

48

52

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

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

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

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

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

55+putCharLn c = putStrLn (singleton c)

52

56

53||| Read a string from standard input.

57||| Read a string from standard input.

54getStr : { [STDIO] } Eff String

58getStr : { [STDIO] } Eff String

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

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

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

9

10instance Handler (Exception a) Maybe where

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

14 handle _ (Raise e) k = []

15

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

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

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

18 believe_me (exit 1)

19

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

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

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

39

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

41-- handler can be introduced mid interpretation?

42−

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

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

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

417

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

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

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

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

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

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

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

422

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

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

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

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

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

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

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

427

428instance Quotable TTName TT where

429 quotedTy = `(TTName)

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

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

31 | CantResolve TT

32 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34+ | NoEliminator String TT

34 | UniverseError

35 | UniverseError

35 | ProgramLineComment

36 | ProgramLineComment

36 | Inaccessible TTName

37 | Inaccessible TTName

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

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

8import Prelude.Monad

9import Language.Reflection

10

11+data Arg : Type where

12+ Explicit : TTName -> Raw -> Arg

13+ Implicit : TTName -> Raw -> Arg

14+ Constraint : TTName -> Raw -> Arg

15+

16+data TyDecl : Type where

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

18+

11abstract

19abstract

12data Tactical : Type -> Type where

20data Tactical : Type -> Type where

13 -- obligatory control stuff

21 -- obligatory control stuff

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

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

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

40 prim__Intro : Maybe TTName -> Tactical ()

48 prim__Intro : Maybe TTName -> Tactical ()

41

49

50+ prim__DeclareType : TyDecl -> Tactical ()

51+

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

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

43

53

54+

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

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

45-- Public API

56-- Public API

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

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

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

117rewriteWith : Raw -> Tactical ()

128rewriteWith : Raw -> Tactical ()

118rewriteWith rule = prim__Rewrite rule

129rewriteWith rule = prim__Rewrite rule

119

130

131+declareType : TyDecl -> Tactical ()

132+declareType decl = prim__DeclareType decl

133+

120debug : Tactical a

134debug : Tactical a

121debug = prim__Debug Nothing

135debug = prim__Debug Nothing

122

136

libs/prelude/Prelude.idr+15−5

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

442putStrLn : String -> IO' ffi ()

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

444

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

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

446partial

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

448+print x = putStr (show x)

449+

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

451+partial

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

448−print x = putStrLn (show x)

453+printLn x = putStrLn (show x)

449

454

450||| Read one line of input from stdin

455||| Read one line of input from stdin

451partial

456partial

452getLine : IO' ffi String

457getLine : IO' ffi String

453−getLine = prim_read

458+getLine = prim_read

454

459

455||| Write a single character to stdout

460||| Write a single character to stdout

456partial

461partial

457putChar : Char -> IO ()

462putChar : Char -> IO ()

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

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

464+

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

466+partial

467+putCharLn : Char -> IO ()

468+putCharLn c = putStrLn (singleton c)

459

469

460||| Read a single character from stdin

470||| Read a single character from stdin

461partial

471partial

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

484do_fopen : String -> String -> IO Ptr

494do_fopen : String -> String -> IO Ptr

485do_fopen f m

495do_fopen f m

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

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

487−

497+

488||| Open a file

498||| Open a file

489||| @ f the filename

499||| @ f the filename

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

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

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

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

316

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

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

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

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

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

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

322

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

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

31

32||| Function composition

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

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

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

35

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

37||| @ f the function to flip

samples/binary.idr+1−2

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

41main : IO ()

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

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

44− print (adc n1 n2 b0)

44+ printLn (adc n1 n2 b0)

45

46

47

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

92 rewrite sym (plusZeroRightNeutral c) ;

93 trivial;

94}

95−

samples/interp-alt.idr+2−2

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

77testFac = interp [] eFac 4

78

79main : IO ()

80−main = do print test

80+main = do printLn test

81− print testFac

81+ printLn testFac

samples/interp.idr+1−2

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

88testFac = interp [] eFac 4

89

90main : IO ()

91−main = print testFac

91+main = printLn testFac

92−

samples/javaffi.idr+1−1

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

9main : IO ()

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

11 res <- binom 49 6

12− print res

12+ printLn res

src/Idris/AbsSyntax.hs+47−23

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

360addInstance int n i

361 = do ist <- getIState

362 case lookupCtxt n (idris_classes ist) of

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

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

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

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

365 putIState $ ist { idris_classes = cs }

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

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

367 putIState $ ist { idris_classes = cs }

368 where addI i ins | int = i : ins

369 | chaser n = ins ++ [i]

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

455putIState :: IState -> Idris ()

456putIState = put

457

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

459+updateIState f = do i <- getIState

460+ putIState $ f i

461+

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

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

459withContext ctx name dflt action = do

463withContext ctx name dflt action = do

460 ist <- getIState

464 ist <- getIState

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

547addDeferred = addDeferred' Ref

551addDeferred = addDeferred' Ref

548addDeferredTyCon = addDeferred' (TCon 0 0)

552addDeferredTyCon = addDeferred' (TCon 0 0)

549

553

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

555+addDeferred' :: NameType

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

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

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

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

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

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

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

562+ -- allowed

563+ -> Idris ()

551addDeferred' nt ns

564addDeferred' nt ns

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

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

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

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

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

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

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

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

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

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

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

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

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

1079 = PClass doc info f

1092 = PClass doc info f

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

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

1081 n

1094 n

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

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

1083 pDocs

1096 pDocs

1097+ fds

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

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

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

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

1086 = PInstance doc argDocs info f

1100 = PInstance doc argDocs info f

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

1467

1481

1468-- Add implicit arguments in function calls

1482-- Add implicit arguments in function calls

1469addImplPat :: IState -> PTerm -> PTerm

1483addImplPat :: IState -> PTerm -> PTerm

1470−addImplPat = addImpl' True [] []

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

1471

1485

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

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

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

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

1474

1488

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

1489addImplBoundInf :: 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

1477

1491

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

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

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

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

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

1480addImpl = addImpl' False [] []

1497addImpl = addImpl' False [] []

1481

1498

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

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

1483-- and *not* inside a PHidden

1500-- and *not* inside a PHidden

1484

1501

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

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

1486−addImpl' inpat env infns ist ptm

1503+addImpl' inpat env infns imp_meths ist ptm

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

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

1488 where

1505 where

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

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

1490 ai qq env ds (PRef fc f)

1507 ai qq env ds (PRef fc f)

1491 | f `elem` infns = PInferRef fc f

1508 | 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 []

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

1510 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 [])

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

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

1496 = let lt' = ai qq env ds lt

1513 = let lt' = ai qq env ds lt

1497 rt' = ai qq env ds rt

1514 rt' = ai qq env ds rt

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

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

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

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

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

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

1546 = 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'

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

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

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

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

1533 arity = getPArity ty in

1550 arity = getPArity ty in

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

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

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

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

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

1564 = let ty' = ai qq env ds ty

1581 = let ty' = ai qq env ds ty

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

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

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

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

1566 PPi p n ty' sc'

1585 PPi p n ty' sc'

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

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

1568 = let r' = ai qq env ds r

1587 = let r' = ai qq env ds r

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

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

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

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

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

1588

1607

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

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

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

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

1591 = case lookupDef f (tt_ctxt ist) of

1610 = case lookupDef f (tt_ctxt ist) of

1592 [] -> Right $ PPatvar fc f

1611 [] -> Right $ PPatvar fc f

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

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

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

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

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

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

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

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

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

1599 else Right $ PPatvar fc f

1618 else Right $ PPatvar fc f

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

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

1601 imp _ = True

1620 imp _ = True

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

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

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

1610 vname _ = False

1629 vname _ = False

1611

1630

1612−aiFn inpat expat qq ist fc f ds as

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

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

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

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

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

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

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

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

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

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

1619 [] -> nh

1638 [] -> nh

1620 x -> x

1639 x -> x

1621 case ns' of

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

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

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

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

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

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

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

1626 alts -> Right $

1645 alts -> Right $

1627 PAlternative True $

1646 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'))

1629 (insertImpl ns as)) alts

1648 (insertImpl ns as)) alts

1630 where

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

1631 trimAlts [] alts = alts

1655 trimAlts [] alts = alts

1632 trimAlts ns alts

1656 trimAlts ns alts

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

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

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

1671 PImp p True l n Placeholder :

1695 PImp p True l n Placeholder :

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

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

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

1697 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

1675 case find n imps [] of

1699 case find n imps [] of

1676 Just (tm, imps') ->

1700 Just (tm, imps') ->

1677 PTacImplicit p l n sc tm :

1701 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+20−9

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

184 idris_name :: Int,

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

186 -- ^ Full application LHS on source line

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

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

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

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

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

191+ -- allowed

188 idris_coercions :: [Name],

192 idris_coercions :: [Name],

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

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

190 syntax_rules :: SyntaxRules,

194 syntax_rules :: SyntaxRules,

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

599 Name

603 Name

600 [(Name, t)] -- parameters

604 [(Name, t)] -- parameters

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

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

606+ [Name] -- determining parameters

602 [PDecl' t] -- declarations

607 [PDecl' t] -- declarations

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

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

604 -- class name, parameters, method declarations

609 -- class name, parameters, method declarations

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

631-- For elaborator state

636-- For elaborator state

632data EState = EState {

637data EState = EState {

633 case_decls :: [PDecl],

638 case_decls :: [PDecl],

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

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

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

635 }

641 }

636

642

637−initEState = EState [] []

643+initEState :: EState

644+initEState = EState [] [] []

638

645

639type ElabD a = Elab' EState a

646type ElabD a = Elab' EState a

640

647

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

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

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

694declared (PNamespace _ ds) = concatMap declared ds

701declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

698declared (PDSL n _) = [n]

705declared (PDSL n _) = [n]

699declared (PSyntax _ _) = []

706declared (PSyntax _ _) = []

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

712tldeclared (PParams _ _ ds) = []

719tldeclared (PParams _ _ ds) = []

713tldeclared (PMutual _ ds) = concatMap tldeclared ds

720tldeclared (PMutual _ ds) = concatMap tldeclared ds

714tldeclared (PNamespace _ ds) = concatMap tldeclared ds

721tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

717tldeclared _ = []

724tldeclared _ = []

718

725

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

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

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

729defined (PNamespace _ ds) = concatMap defined ds

736defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

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

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

733defined (PDSL n _) = [n]

740defined (PDSL n _) = [n]

734defined (PSyntax _ _) = []

741defined (PSyntax _ _) = []

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

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

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

1030 class_default_superclasses :: [PDecl],

1037 class_default_superclasses :: [PDecl],

1031 class_params :: [Name],

1038 class_params :: [Name],

1032− class_instances :: [Name] }

1039+ class_instances :: [Name],

1040+ class_determiners :: [Int] }

1033 deriving Show

1041 deriving Show

1034{-!

1042{-!

1035deriving instance Binary ClassInfo

1043deriving instance Binary ClassInfo

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

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

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

1191 syn_namespace :: [String],

1199 syn_namespace :: [String],

1192 no_imp :: [Name],

1200 no_imp :: [Name],

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

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

1203+ -- binders

1193 decoration :: Name -> Name,

1204 decoration :: Name -> Name,

1194 inPattern :: Bool,

1205 inPattern :: Bool,

1195 implicitAllowed :: Bool,

1206 implicitAllowed :: Bool,

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

1203deriving instance Binary SyntaxInfo

1214deriving instance Binary SyntaxInfo

1204!-}

1215!-}

1205

1216

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

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

1207

1218

1208expandNS :: SyntaxInfo -> Name -> Name

1219expandNS :: SyntaxInfo -> Name -> Name

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

91 put x

92 put y

93 put z

94− put (CantResolve t) = do putWord8 15

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

95− put t

95+ put t

96 put (CantResolveAlts ns) = do putWord8 16

97 put ns

98 put (IncompleteTerm t) = do putWord8 17

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

146 put x1

147 put x2

148 put x3

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

150+ put s

151+ put t

149

152

150 get = do i <- getWord8

153 get = do i <- getWord8

151 case i of

154 case i of

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

172 13 -> fmap NoTypeDecl get

175 13 -> fmap NoTypeDecl get

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

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

174 return $ NotInjective x y z

177 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

176 16 -> fmap CantResolveAlts get

179 16 -> fmap CantResolveAlts get

177 17 -> fmap IncompleteTerm get

180 17 -> fmap IncompleteTerm get

178 18 -> return UniverseError

181 18 -> return UniverseError

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

205 x2 <- get

208 x2 <- get

206 x3 <- get

209 x3 <- get

207 return (ElabDebug x1 x2 x3)

210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

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

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

209----- Generated by 'derive'

215----- Generated by 'derive'

210

216

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

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

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

81 rnf (NotInjective x1 x2 x3)

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

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

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

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

86 rnf UniverseError = ()

87 rnf UniverseError = ()

87 rnf ProgramLineComment = ()

88 rnf ProgramLineComment = ()

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

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

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

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

756

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

758try' t1 t2 proofSearch

759− = do s <- get

759+ = do s <- get

760− ps <- get_probs

760+ ps <- get_probs

761− ulog <- getUnifyLog

761+ ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

762+ case prunStateT 999999 False ps t1 s of

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

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

764− return $! v

764+ return $! v

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

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

766− if recoverableErr e1 then

766+ if recoverableErr e1 then

767− do case runStateT t2 s of

767+ do case runStateT t2 s of

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

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

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

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

770− then lift (tfail e1)

770+ then lift (tfail e1)

771− else lift (tfail e2)

771+ else lift (tfail e2)

772− else lift (tfail e1)

772+ else lift (tfail e1)

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

774 = -- traceWhen r (show err) $

775 r || proofSearch

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

782 recoverableErr (ElabDebug _ _ _) = False

783 recoverableErr _ = True

784

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

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

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

792+ return $! v

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

794+ case runStateT (t2 e1) s of

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

796+ return $! v

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

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

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

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

786tryWhen True a b = try a b

802tryWhen True a b = try a b

787tryWhen False a b = a

803tryWhen False a b = a

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

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

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

682 let tmt' = normalise ctxt env tmt

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

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

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

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

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

686 case unApply tmt' of

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

688 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

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

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

719 return scv'

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

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

721 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'

723 where scname = sMN 0 "scarg"

724 where scname = sMN 0 "scarg"

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

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

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

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

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

878 ctxt = context ps

879 ctxt = context ps

879 ulog = unifylog ps

880 ulog = unifylog ps

880 usupp = map fst (notunified ps)

881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

881

883

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

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

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

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

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

889 if newx || newy || ready ||

891 if newx || newy || ready ||

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

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

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

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

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

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

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

893− up (ns ++ v) ps

896+ up (ns ++ v') ps

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

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

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

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

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

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

src/Idris/Core/ProofTerm.hs+3

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

172 else (t, False)

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

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

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

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

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

175 updateSolved' xs t = (t, False)

178 updateSolved' xs t = (t, False)

176

179

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

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

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

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

155 | WithFnType t

156 | NoTypeDecl Name

157 | NotInjective t t t

158− | CantResolve t

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

159+ t

159 | CantResolveAlts [Name]

160 | CantResolveAlts [Name]

160 | IncompleteTerm t

161 | IncompleteTerm t

162+ | NoEliminator String t

161 | UniverseError

163 | UniverseError

162 | UniqueError Universe Name

164 | UniqueError Universe Name

163 | UniqueKindError Universe Name

165 | UniqueKindError Universe Name

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

231 size (NoSuchVariable name) = size name

233 size (NoSuchVariable name) = size name

232 size (NoTypeDecl name) = size name

234 size (NoTypeDecl name) = size name

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

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

234− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

235 size (NoRewriting trm) = size trm

237 size (NoRewriting trm) = size trm

236 size (CantResolveAlts _) = 1

238 size (CantResolveAlts _) = 1

237 size (IncompleteTerm trm) = size trm

239 size (IncompleteTerm trm) = size trm

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

246

248

247score :: Err -> Int

249score :: Err -> Int

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

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

249−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

250score (NoSuchVariable _) = 1000

252score (NoSuchVariable _) = 1000

251score (ProofSearchFail e) = score e

253score (ProofSearchFail e) = score e

252score (CantSolveGoal _ _) = 100000

254score (CantSolveGoal _ _) = 100000

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

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

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

508 concatMap (Map.toList) allns

510 concatMap (Map.toList) allns

509

511

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

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

511addAlist [] ctxt = ctxt

513addAlist [] ctxt = ctxt

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

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

513

515

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

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

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

935instantiate :: TT n -> TT n -> TT n

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

936instantiate e = subst 0 where

938instantiate e = subst 0 where

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

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

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

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

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

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

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

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

945-- that has been substituted.

948-- that has been substituted.

946substV :: TT n -> TT n -> TT n

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

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

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

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

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

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

949 | otherwise = V x

953 | otherwise = V x

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

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

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

1038 -- substitution happens...)

1042 -- substitution happens...)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

101 holeIn env f || f `elem` holes

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

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

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

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

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

106 holeIn env f || f `elem` holes

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

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

111 holeIn env f || f `elem` holes

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

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

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

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

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

116 holeIn env f || f `elem` holes

src/Idris/Coverage.hs+1−1

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

24-- provided explicitly from new clause generation.

25mkPatTm :: PTerm -> Idris Term

26mkPatTm t = do i <- getIState

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

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

28 evalStateT (toTT (mapPT deNS timp)) 0

29 where

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

src/Idris/DeepSeq.hs+6−6

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

149 rnf x2 `seq`

150 rnf x3 `seq`

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

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

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

153 = rnf x1 `seq`

154 rnf x2 `seq`

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

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

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

157 = rnf x1 `seq`

158 rnf x2 `seq`

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

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

314

315instance NFData ClassInfo where

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

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

317 = rnf x1 `seq`

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

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

319

320instance NFData OptInfo where

321 rnf (Optimise x1 x2)

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

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

354

355instance 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)

357 = rnf x1 `seq`

358 rnf x2 `seq`

359 rnf x3 `seq`

360 rnf x4 `seq`

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

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

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

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

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

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

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

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

299pprintErr' i (CantMatch t) =

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

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

302+pprintErr' i (NoEliminator s t)

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

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

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

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

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

302pprintErr' i UniverseError = text "Universe inconsistency"

308pprintErr' i UniverseError = text "Universe inconsistency"

303pprintErr' i (UniqueError NullType n)

309pprintErr' i (UniqueError NullType n)

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

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

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

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

50

51import Util.Pretty(pretty, text)

52

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

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

54

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

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

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

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

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

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

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

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

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

60 let tty = pibind ps PType

61 let tty = pibind ps PType

61 let constraint = PApp fc (PRef fc tn)

62 let constraint = PApp fc (PRef fc tn)

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

75 let (methods, imethods)

76 let (methods, imethods)

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

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

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

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

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

79 -- build instance constructor type

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

81− -- to elsewhere in the class declaration

82 let cty = impbind ps $ conbind constraints

80 let cty = impbind ps $ conbind constraints

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

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

84 constraint

82 constraint

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

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

86 let ddecl = PDatadecl tn tty cons

84 let ddecl = PDatadecl tn tty cons

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

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

86+ -- Elaborate the data declaration

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

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+

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

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

90− logLvl 5 $ "Building functions"

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

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

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

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

95+

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

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

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

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

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

99+ -- Elaborate the the top level methods

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

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

101+

98 -- add the default definitions

102 -- add the default definitions

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

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

100 addIBC (IBCClass tn)

104 addIBC (IBCClass tn)

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

130

134

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

203

207

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

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

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

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

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

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

207 getMArgs _ = []

211 getMArgs _ = []

208

212

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

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

210 | otherwise = getMeth ms as x

214 | otherwise = getMeth ms as x

211

215

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

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

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

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

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

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

215 lhsArgs [] _ = []

219 lhsArgs [] _ = []

216

220

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

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

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

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

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

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

220 rhsArgs [] _ = []

224 rhsArgs [] _ = []

221

225

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

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

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

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

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

232 toExp ns e sc = sc

236 toExp ns e sc = sc

237+

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

239+findDets n ns =

240+ do i <- getIState

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

242+ Just ty -> getDetPos 0 ns ty

243+ Nothing -> []

244+ where

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

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

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

248+ getDetPos _ _ _ = []

249+

250+

src/Idris/Elab/Clause.hs+35−23

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

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

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

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

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

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

459+ do setContext ctxt'

460+ processTacticDecls newDecls

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

461+ let lhs_tm = orderPats (getInferTerm lhs')

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

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

461 OK _ -> return True

463 OK _ -> return True

462 err -> return False

464 err -> return False

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

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

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

547 = do let tcgen = Dictionary `elem` opts

549 = do let tcgen = Dictionary `elem` opts

548 i <- get

550 i <- get

549− let lhs = addImpl i lhs_in

551+ let lhs = addImpl [] i lhs_in

550 b <- checkPossible info fc tcgen fname lhs_in

552 b <- checkPossible info fc tcgen fname lhs_in

551 case b of

553 case b of

552 True -> tclift $ tfail (At fc

554 True -> tclift $ tfail (At fc

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

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

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

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

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

581

583

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

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

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

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

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

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

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

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

586− probs <- get_probs

588+ probs <- get_probs

587− inj <- get_inj

589+ inj <- get_inj

588− return (res, probs, inj))

590+ return (res, probs, inj))

589−

591+ setContext ctxt'

592+ processTacticDecls newDecls

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

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

591

594

592 let lhs_tm = orderPats (getInferTerm lhs')

595 let lhs_tm = orderPats (getInferTerm lhs')

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

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

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

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

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

655 logLvl 5 "STARTING CHECK"

658 logLvl 5 "STARTING CHECK"

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

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

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

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

658 (do pbinds ist lhs_tm

661 (do pbinds ist lhs_tm

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

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

660 setNextName

663 setNextName

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

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

665+ errAt "right hand side of " fname

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

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

663 errAt "right hand side of " fname

667 errAt "right hand side of " fname

664 (erun fc $ psolve lhs_tm)

668 (erun fc $ psolve lhs_tm)

665 hs <- get_holes

669 hs <- get_holes

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

668 tt <- get_term

672 tt <- get_term

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

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

670 probs <- get_probs

674 probs <- get_probs

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

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

672−

676+ setContext ctxt'

677+ processTacticDecls newDecls

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

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

674

679

675 logLvl 5 "DONE CHECK"

680 logLvl 5 "DONE CHECK"

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

812 let params = getParamsInType i [] fn_is fn_ty

817 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

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

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

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

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

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

824+ setContext ctxt'

825+ processTacticDecls newDecls

819 let lhs_tm = orderPats (getInferTerm lhs')

826 let lhs_tm = orderPats (getInferTerm lhs')

820 let lhs_ty = getInferType lhs'

827 let lhs_ty = getInferType lhs'

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

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

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

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

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

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

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

829 -- Elaborate wval in this context

836 -- Elaborate wval in this context

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

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

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

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

832 (bindTyArgs PVTy bargs infP) initEState

839 (bindTyArgs PVTy bargs infP) initEState

833 (do pbinds i lhs_tm

840 (do pbinds i lhs_tm

834 setNextName

841 setNextName

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

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

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

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

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

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

838 erun fc $ psolve lhs_tm

845 erun fc $ psolve lhs_tm

839 tt <- get_term

846 tt <- get_term

840− return (tt, d, is))

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

848+ setContext ctxt'

849+ processTacticDecls newDecls

841 def' <- checkDef fc defer

850 def' <- checkDef fc defer

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

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

843 addDeferred def''

852 addDeferred def''

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

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

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

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

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

925 i <- getIState

934 i <- getIState

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

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

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

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

928 (do pbinds i lhs_tm

937 (do pbinds i lhs_tm

929 setNextName

938 setNextName

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

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

931 psolve lhs_tm

940 psolve lhs_tm

932 tt <- get_term

941 tt <- get_term

933− return (tt, d, is))

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

943+ setContext ctxt'

944+ processTacticDecls newDecls

945+

934 def' <- checkDef fc defer

946 def' <- checkDef fc defer

935 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

947 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

936 addDeferred def''

948 addDeferred def''

src/Idris/Elab/Data.hs+2−1

@@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

215 Idris (Name, Type)

216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217 = do checkUndefined fc n

218+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

218 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219 ctxt <- getContext

220 ctxt <- getContext

220 let cty' = normalise ctxt [] cty

221 let cty' = normalise ctxt [] cty

@@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

223 -- Check that the constructor type is, in fact, a part of the family being defined

224 -- Check that the constructor type is, in fact, a part of the family being defined

224 tyIs n cty'

225 tyIs n cty'

225

226

226− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

227+ logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

227 logLvl 5 $ "Inaccessible args: " ++ show inacc

228 logLvl 5 $ "Inaccessible args: " ++ show inacc

228 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229

230

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

75 -- if the instance type matches any of the instances we have already,

76 -- and it's not a named instance, then it's overlapping, so report an error

77 case expn of

78− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))

78+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (class_determiners ci) (delab i nty))

79 (class_instances ci)

80 addInstance intInst n iname

81 Just _ -> addInstance intInst n iname

@@ -167,33 +167,45 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

167 = do ty' <- addUsingConstraints syn fc t

168 -- TODO think: something more in info?

169 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

170+ let ty = addImpl [] i ty'

171 ctxt <- getContext

172− ((tyT, _, _), _) <-

172+ (ElabResult tyT _ _ ctxt' newDecls, _) <-

173− tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

173+ tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

174− (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

174+ (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

175+ setContext ctxt'

176+ processTacticDecls newDecls

175 ctxt <- getContext

177 ctxt <- getContext

176 (cty, _) <- recheckC fc [] tyT

178 (cty, _) <- recheckC fc [] tyT

177 let nty = normalise ctxt [] cty

179 let nty = normalise ctxt [] cty

178− return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)

180+ return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)

179

181

180− findOverlapping i t n

182+ findOverlapping i dets t n

181 | take 2 (show n) == "@@" = Nothing

183 | take 2 (show n) == "@@" = Nothing

182 | otherwise

184 | otherwise

183 = case lookupTy n (tt_ctxt i) of

185 = case lookupTy n (tt_ctxt i) of

184 [t'] -> let tret = getRetType t

186 [t'] -> let tret = getRetType t

185 tret' = getRetType (delab i t') in

187 tret' = getRetType (delab i t') in

186− case matchClause i tret' tret of

188+ case matchArgs i dets tret' tret of

187− Right ms -> Just tret'

189+ Right _ -> Just tret'

188− Left _ -> case matchClause i tret tret' of

190+ Left _ -> case matchArgs i dets tret tret' of

189− Right ms -> Just tret'

191+ Right _ -> Just tret'

190− Left _ -> Nothing

192+ Left _ -> Nothing

191 _ -> Nothing

193 _ -> Nothing

192 overlapping t' = tclift $ tfail (At fc (Msg $

194 overlapping t' = tclift $ tfail (At fc (Msg $

193 "Overlapping instance: " ++ show t' ++ " already defined"))

195 "Overlapping instance: " ++ show t' ++ " already defined"))

194 getRetType (PPi _ _ _ sc) = getRetType sc

196 getRetType (PPi _ _ _ sc) = getRetType sc

195 getRetType t = t

197 getRetType t = t

196

198

199+ matchArgs i dets x y =

200+ let x' = keepDets dets x

201+ y' = keepDets dets y in

202+ matchClause i x' y'

203+

204+ keepDets dets (PApp fc f args)

205+ = PApp fc f $ let a' = zip [0..] args in

206+ map snd (filter (\(i, _) -> i `elem` dets) a')

207+ keepDets dets t = t

208+

197 mkMethApp (n, _, _, ty)

209 mkMethApp (n, _, _, ty)

198 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

210 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

199 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

211 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

src/Idris/Elab/Transform.hs+10−4

@@ -53,10 +53,12 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56− ((lhs', dlhs, []), _) <-

56+ (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

57 tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState

58 (erun fc (buildTC i info ELHS [] (sUN "transform")

59 (infTerm lhs)))

60+ setContext ctxt'

61+ processTacticDecls newDecls

60 let lhs_tm = orderPats (getInferTerm lhs')

62 let lhs_tm = orderPats (getInferTerm lhs')

61 let lhs_ty = getInferType lhs'

63 let lhs_ty = getInferType lhs'

62 let newargs = pvars i lhs_tm

64 let newargs = pvars i lhs_tm

@@ -66,14 +68,18 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

66 logLvl 3 ("Transform LHS " ++ show clhs_tm)

68 logLvl 3 ("Transform LHS " ++ show clhs_tm)

67

69

68 let rhs = addImplBound i (map fst newargs) rhs_in

70 let rhs = addImplBound i (map fst newargs) rhs_in

69− ((rhs', defer), _) <-

71+ ((rhs', defer, ctxt', newDecls), _) <-

70 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

72 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

71 (do pbinds i lhs_tm

73 (do pbinds i lhs_tm

72 setNextName

74 setNextName

73− erun fc (build i info ERHS [] (sUN "transform") rhs)

75+ (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

74 erun fc $ psolve lhs_tm

76 erun fc $ psolve lhs_tm

75 tt <- get_term

77 tt <- get_term

76− return (runState (collectDeferred Nothing tt) []))

78+ let (rhs', defer) = runState (collectDeferred Nothing tt) []

79+ return (rhs', defer, ctxt', newDecls))

80+ setContext ctxt'

81+ processTacticDecls newDecls

82+

77 (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

83 (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

78 let crhs_tm = renamepats pnames crhs_tm_in

84 let crhs_tm = renamepats pnames crhs_tm_in

79 logLvl 3 ("Transform RHS " ++ show crhs_tm)

85 logLvl 3 ("Transform RHS " ++ show crhs_tm)

src/Idris/Elab/Type.hs+14−10

@@ -57,17 +57,19 @@ buildType info syn fc opts n ty' = do

57 ctxt <- getContext

58 i <- getIState

59

60− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

60+ logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

61 ty' <- addUsingConstraints syn fc ty'

62 ty' <- addUsingImpls syn n fc ty'

63− let ty = addImpl i ty'

63+ let ty = addImpl (imp_methods syn) i ty'

64

65− logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

65+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66− logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

66+ logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

67

68− ((tyT', defer, is), log) <-

68+ (ElabResult tyT' defer is ctxt' newDecls, log) <-

69− tclift $ elaborate ctxt n (TType (UVal 0)) initEState

69+ tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

70+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

71+ setContext ctxt'

72+ processTacticDecls newDecls

71

73

72 let tyT = patToImp tyT'

74 let tyT = patToImp tyT'

73

75

@@ -114,12 +116,14 @@ buildType info syn fc opts n ty' = do

114 param_pos i ns t = []

116 param_pos i ns t = []

115

117

116-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

118-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

119+elabType :: ElabInfo -> SyntaxInfo

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

120+ -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

118− FC -> FnOpts -> Name -> PTerm -> Idris Type

121+ -> FC -> FnOpts -> Name -> PTerm -> Idris Type

119elabType = elabType' False

122elabType = elabType' False

120

123

121elabType' :: Bool -> -- normalise it

124elabType' :: Bool -> -- normalise it

125+ ElabInfo -> SyntaxInfo ->

122− ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

126+ Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

123 FC -> FnOpts -> Name -> PTerm -> Idris Type

127 FC -> FnOpts -> Name -> PTerm -> Idris Type

124elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

128elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125 n = liftname info n_in in -}

129 n = liftname info n_in in -}

src/Idris/Elab/Utils.hs+10−8

@@ -22,7 +22,7 @@ import Debug.Trace

22

23import qualified Data.Map as Map

24

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

26

27recheckC_borrowing uniq_check bs fc env t

28 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

@@ -34,9 +34,13 @@ recheckC_borrowing uniq_check bs fc env t

34 addConstraints fc cs

35 return (tm, ty)

36

37−

37+checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]

38+ -> Idris [(Name, (Int, Maybe Name, Type))]

38checkDef fc ns = checkAddDef False True fc ns

39checkDef fc ns = checkAddDef False True fc ns

39

40

41+checkAddDef :: Bool -> Bool -> FC

42+ -> [(Name, (Int, Maybe Name, Type))]

43+ -> Idris [(Name, (Int, Maybe Name, Type))]

40checkAddDef add toplvl fc [] = return []

44checkAddDef add toplvl fc [] = return []

41checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

45checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

42 = do ctxt <- getContext

46 = do ctxt <- getContext

@@ -46,7 +50,7 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

46 ns' <- checkAddDef add toplvl fc ns

50 ns' <- checkAddDef add toplvl fc ns

47 return ((n, (i, top, t')) : ns')

51 return ((n, (i, top, t')) : ns')

48

52

49−-- Get the list of (index, name) of inaccessible arguments from an elaborated

53+-- | Get the list of (index, name) of inaccessible arguments from an elaborated

50-- type

54-- type

51inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

55inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

52inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

56inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

@@ -54,7 +58,7 @@ inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

54 | otherwise = inaccessibleImps (i + 1) sc ins

58 | otherwise = inaccessibleImps (i + 1) sc ins

55inaccessibleImps _ _ _ = []

59inaccessibleImps _ _ _ = []

56

60

57−-- Get the list of (index, name) of inaccessible arguments from the type.

61+-- | Get the list of (index, name) of inaccessible arguments from the type.

58inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

62inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

59inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

63inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

60 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

64 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

@@ -74,10 +78,9 @@ elabCaseBlock info opts d@(PClauses f o n ps)

74 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

78 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

75 rec_elabDecl info EAll info (PClauses f opts' n ps )

79 rec_elabDecl info EAll info (PClauses f opts' n ps )

76

80

77−-- Check that the result of type checking matches what the programmer wrote

81+-- | Check that the result of type checking matches what the programmer wrote

78-- (i.e. - if we inferred any arguments that the user provided, make sure

82-- (i.e. - if we inferred any arguments that the user provided, make sure

79-- they are the same!)

83-- they are the same!)

80−

81checkInferred :: FC -> PTerm -> PTerm -> Idris ()

84checkInferred :: FC -> PTerm -> PTerm -> Idris ()

82checkInferred fc inf user =

85checkInferred fc inf user =

83 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

86 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

@@ -92,9 +95,8 @@ checkInferred fc inf user =

92 logLvl 10 $ "Checked match"

95 logLvl 10 $ "Checked match"

93-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

96-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

94

97

95−-- Return whether inferred term is different from given term

98+-- | Return whether inferred term is different from given term

96-- (as above, but return a Bool)

99-- (as above, but return a Bool)

97−

98inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

100inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

99inferredDiff fc inf user =

101inferredDiff fc inf user =

100 do i <- getIState

102 do i <- getIState

src/Idris/Elab/Value.hs+9−4

@@ -56,16 +56,21 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam

56elabValBind info aspat norm tm_in

57 = do ctxt <- getContext

58 i <- getIState

59− let tm = addImpl i tm_in

59+ let tm = addImpl [] i tm_in

60 logLvl 10 (showTmImpls tm)

61 -- try:

62 -- * ordinary elaboration

63 -- * elaboration as a Type

64 -- * elaboration as a function a -> b

65

66− ((tm', defer, is), _) <-

66+ (ElabResult tm' defer is ctxt' newDecls, _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP initEState

67+ tclift (elaborate ctxt (sMN 0 "val") infP initEState

68− (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

68+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

69+

70+ -- Extend the context with new definitions created

71+ setContext ctxt'

72+ processTacticDecls newDecls

73+

69 let vtm = orderPats (getInferTerm tm')

74 let vtm = orderPats (getInferTerm tm')

70

75

71 def' <- checkDef (fileFC "(input)") defer

76 def' <- checkDef (fileFC "(input)") defer

src/Idris/ElabDecls.hs+2−2

@@ -229,10 +229,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

229 ninfo = case namespace info of

230 Nothing -> info { namespace = Just [n] }

231 Just ns -> info { namespace = Just (n:ns) }

232−elabDecl' what info (PClass doc s f cs n ps pdocs ds)

232+elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)

233 | what /= EDefns

234 = do iLOG $ "Elaborating class " ++ show n

235− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

235+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds

236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237 = do iLOG $ "Elaborating instance " ++ show n

238 elabInstance info s doc argDocs what f cs n ps t expn ds

src/Idris/ElabTerm.hs+210−81

@@ -18,6 +18,7 @@ import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20import Idris.Elab.Utils

21+import Idris.Reflection

21import qualified Util.Pretty as U

22import qualified Util.Pretty as U

22

23

23import Control.Applicative ((<$>))

24import Control.Applicative ((<$>))

@@ -36,6 +37,32 @@ import Debug.Trace

36data ElabMode = ETyDecl | ELHS | ERHS

37data ElabMode = ETyDecl | ELHS | ERHS

37 deriving Eq

38 deriving Eq

38

39

40+data ElabResult =

41+ ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

42+ , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

43+ -- ^ Information about new metavariables

44+ , resultCaseDecls :: [PDecl]

45+ -- ^ Deferred declarations as the meaning of case blocks

46+ , resultContext :: Context

47+ -- ^ The potentially extended context from new definitions

48+ , resultTyDecls :: [(Name, FC, [PArg], Type)]

49+ -- ^ Meta-info about the new type declarations

50+ }

51+

52+processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()

53+processTacticDecls info =

54+ forM_ info $ \(n, fc, impls, ty) ->

55+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

56+ logLvl 3 $ " It has impls " ++ show impls

57+ updateIState $ \i -> i { idris_implicits =

58+ addDef n impls (idris_implicits i) }

59+ addIBC (IBCImp n)

60+ ds <- checkDef fc [(n, (-1, Nothing, ty))]

61+ addIBC (IBCDef n)

62+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

63+ addDeferred ds'

64+

65+

39-- Using the elaborator, convert a term in raw syntax to a fully

66-- Using the elaborator, convert a term in raw syntax to a fully

40-- elaborated, typechecked term.

67-- elaborated, typechecked term.

41--

68--

@@ -45,7 +72,7 @@ data ElabMode = ETyDecl | ELHS | ERHS

45-- Also find deferred names in the term and their types

72-- Also find deferred names in the term and their types

46

73

47build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

74build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

48− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

75+ ElabD ElabResult

49build ist info emode opts fn tm

76build ist info emode opts fn tm

50 = do elab ist info emode opts fn tm

77 = do elab ist info emode opts fn tm

51 let tmIn = tm

78 let tmIn = tm

@@ -64,7 +91,7 @@ build ist info emode opts fn tm

64 mapM_ (\n -> when (n `elem` hs) $

91 mapM_ (\n -> when (n `elem` hs) $

65 do focus n

92 do focus n

66 g <- goal

93 g <- goal

67− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

68 (movelast n)) ivs

95 (movelast n)) ivs

69 ivs <- get_instances

96 ivs <- get_instances

70 hs <- get_holes

97 hs <- get_holes

@@ -72,7 +99,8 @@ build ist info emode opts fn tm

72 mapM_ (\n -> when (n `elem` hs) $

99 mapM_ (\n -> when (n `elem` hs) $

73 do focus n

100 do focus n

74 g <- goal

101 g <- goal

102+ ptm <- get_term

75− resolveTC True 7 g fn ist) ivs

103+ resolveTC True True 7 g fn ist) ivs

76 tm <- get_term

104 tm <- get_term

77 ctxt <- get_context

105 ctxt <- get_context

78 probs <- get_probs

106 probs <- get_probs

@@ -94,12 +122,13 @@ build ist info emode opts fn tm

94 when tydecl (do update_term orderPats

122 when tydecl (do update_term orderPats

95 mkPat)

123 mkPat)

96-- update_term liftPats)

124-- update_term liftPats)

97− EState is _ <- getAux

125+ EState is _ impls <- getAux

98 tt <- get_term

126 tt <- get_term

99 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

100 log <- getLog

128 log <- getLog

129+ ctxt <- get_context

101− if (log /= "") then trace log $ return (tm, ds, is)

130+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

102− else return (tm, ds, is)

131+ else return (ElabResult tm ds is ctxt impls)

103 where pattern = emode == ELHS

132 where pattern = emode == ELHS

104 tydecl = emode == ETyDecl

133 tydecl = emode == ETyDecl

105

134

@@ -114,7 +143,7 @@ build ist info emode opts fn tm

114-- know about yet on the LHS of a pattern def)

143-- know about yet on the LHS of a pattern def)

115

144

116buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

145buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

117− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

146+ ElabD ElabResult

118buildTC ist info emode opts fn tm

147buildTC ist info emode opts fn tm

119 = do -- set name supply to begin after highest index in tm

148 = do -- set name supply to begin after highest index in tm

120 let ns = allNamesIn tm

149 let ns = allNamesIn tm

@@ -135,12 +164,13 @@ buildTC ist info emode opts fn tm

135 -- unification

164 -- unification

136 when (not (null dots)) $

165 when (not (null dots)) $

137 lift (Error (CantMatch (getInferTerm tm)))

166 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

167+ EState is _ impls <- getAux

139 tt <- get_term

168 tt <- get_term

140 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

169 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

141 log <- getLog

170 log <- getLog

171+ ctxt <- get_context

142− if (log /= "") then trace log $ return (tm, ds, is)

172+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

143− else return (tm, ds, is)

173+ else return (ElabResult tm ds is ctxt impls)

144 where pattern = emode == ELHS

174 where pattern = emode == ELHS

145

175

146-- return whether arguments of the given constructor name can be

176-- return whether arguments of the given constructor name can be

@@ -183,9 +213,9 @@ goal_polymorphic =

183 _ -> return True

213 _ -> return True

184 _ -> return False

214 _ -> return False

185

215

186−-- Returns the set of declarations we need to add to complete the definition

216+-- | Returns the set of declarations we need to add to complete the

187−-- (most likely case blocks to elaborate)

217+-- definition (most likely case blocks to elaborate) as well as

188−

218+-- declarations resulting from user tactic scripts (%runTactics)

189elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

219elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

190 ElabD ()

220 ElabD ()

191elab ist info emode opts fn tm

221elab ist info emode opts fn tm

@@ -321,7 +351,7 @@ elab ist info emode opts fn tm

321 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

351 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322 _ -> elab' ina (Just fc) (PRef fc unitCon)

352 _ -> elab' ina (Just fc) (PRef fc unitCon)

323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

353 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

324− = do g <- goal; resolveTC False 5 g fn ist

354+ = do g <- goal; resolveTC False False 5 g fn ist

325 elab' ina fc (PResolveTC fc')

355 elab' ina fc (PResolveTC fc')

326 = do c <- getNameFrom (sMN 0 "class")

356 = do c <- getNameFrom (sMN 0 "class")

327 instanceArg c

357 instanceArg c

@@ -540,7 +570,7 @@ elab ist info emode opts fn tm

540 g <- goal

570 g <- goal

541 hs <- get_holes

571 hs <- get_holes

542 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

572 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

543− then try (resolveTC True 7 g fn ist)

573+ then try (resolveTC True False 7 g fn ist)

544 (movelast n)

574 (movelast n)

545 else movelast n)

575 else movelast n)

546 (ivs' \\ ivs)

576 (ivs' \\ ivs)

@@ -700,7 +730,7 @@ elab ist info emode opts fn tm

700 env <- get_env

730 env <- get_env

701 hs <- get_holes

731 hs <- get_holes

702 if all (\n -> not (n `elem` hs)) (freeNames g)

732 if all (\n -> not (n `elem` hs)) (freeNames g)

703− then try (resolveTC False 7 g fn ist)

733+ then try (resolveTC False False 7 g fn ist)

704 (movelast n)

734 (movelast n)

705 else movelast n)

735 else movelast n)

706 (ivs' \\ ivs)

736 (ivs' \\ ivs)

@@ -965,17 +995,14 @@ elab ist info emode opts fn tm

965 elab' ina fc (PUnifyLog t) = do unifyLog True

995 elab' ina fc (PUnifyLog t) = do unifyLog True

966 elab' ina fc t

996 elab' ina fc t

967 unifyLog False

997 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

969 = do -- First extract the unquoted subterms, replacing them with fresh

999 = do -- First extract the unquoted subterms, replacing them with fresh

970 -- names in the quasiquoted term. Claim their reflections to be

1000 -- names in the quasiquoted term. Claim their reflections to be

971 -- an inferred type (to support polytypic quasiquotes).

1001 -- an inferred type (to support polytypic quasiquotes).

1002+ finalTy <- goal

972 (t, unq) <- extractUnquotes 0 t

1003 (t, unq) <- extractUnquotes 0 t

973 let unquoteNames = map fst unq

1004 let unquoteNames = map fst unq

974− mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")

975− claim uqh RType

976− movelast uqh

977− claim uqn (Var uqh)) unquoteNames

1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames

978−

979

1006

980 -- Save the old state - we need a fresh proof state to avoid

1007 -- Save the old state - we need a fresh proof state to avoid

981 -- capturing lexically available variables in the quoted term.

1008 -- capturing lexically available variables in the quoted term.

@@ -1010,7 +1037,7 @@ elab ist info emode opts fn tm

1010 letbind nTm (Var qTy) (Var qTm)

1037 letbind nTm (Var qTy) (Var qTm)

1011

1038

1012 -- Fill out the goal type, if relevant

1039 -- Fill out the goal type, if relevant

1013− case goal of

1040+ case goalt of

1014 Nothing -> return ()

1041 Nothing -> return ()

1015 Just gTy -> do focus qTy

1042 Just gTy -> do focus qTy

1016 elabE (ina { e_qq = True }) fc gTy

1043 elabE (ina { e_qq = True }) fc gTy

@@ -1025,18 +1052,20 @@ elab ist info emode opts fn tm

1025 env <- get_env

1052 env <- get_env

1026 loadState

1053 loadState

1027 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1054 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1028−

1055+ isRaw = case unApply (normaliseAll ctxt env finalTy) of

1056+ (P _ n _, []) | n == reflm "Raw" -> True

1057+ _ -> False

1029 case quoted of

1058 case quoted of

1030 Just q -> do ctxt <- get_context

1059 Just q -> do ctxt <- get_context

1031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1032 if pattern

1061 if pattern

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1033− then do try' (reflectTTQuotePattern unquoteNames q')

1064+ else reflectTTQuotePattern unquoteNames q'

1034− (reflectRawQuotePattern unquoteNames (forget q'))

1065+ else do if isRaw

1035− True

1036− else do try' (fill $ reflectTTQuote unquoteNames q')

1037− -- we forget q' instead of using q to ensure rechecking

1066+ then -- we forget q' instead of using q to ensure rechecking

1038− (fill $ reflectRawQuote unquoteNames (forget q'))

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1039− True -- ignore errors like proof search does

1068+ else fill $ reflectTTQuote unquoteNames q'

1040 solve

1069 solve

1041

1070

1042 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

1071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

@@ -1077,8 +1106,8 @@ elab ist info emode opts fn tm

1077 focus n

1106 focus n

1078 elab' ina (Just fc') tm

1107 elab' ina (Just fc') tm

1079 env <- get_env

1108 env <- get_env

1080− ctxt <- get_context

1081− runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)

1109+ runTactical (maybe fc' id fc) env (P Bound n' Erased)

1110+ EState _ _ todo <- getAux

1082 solve

1111 solve

1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1084

1113

@@ -1346,7 +1375,7 @@ findInstances :: IState -> Term -> [Name]

1346findInstances ist t

1375findInstances ist t

1347 | (P _ n _, _) <- unApply t

1376 | (P _ n _, _) <- unApply t

1348 = case lookupCtxt n (idris_classes ist) of

1377 = case lookupCtxt n (idris_classes ist) of

1349− [CI _ _ _ _ _ ins] -> ins

1378+ [CI _ _ _ _ _ ins _] -> ins

1350 _ -> []

1379 _ -> []

1351 | otherwise = []

1380 | otherwise = []

1352

1381

@@ -1376,14 +1405,26 @@ proofSearch' ist rec ambigok depth prv top n hints

1376-- Resolve type classes. This will only pick up 'normal' instances, never

1405-- Resolve type classes. This will only pick up 'normal' instances, never

1377-- named instances (hence using 'tcname' to check it's a generated instance

1406-- named instances (hence using 'tcname' to check it's a generated instance

1378-- name).

1407-- name).

1408+resolveTC :: Bool -- using default Int

1409+ -> Bool -- allow metavariables in the goal

1410+ -> Int -- depth

1411+ -> Term -- top level goal

1412+ -> Name -- top level function name

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1413+ -> IState -> ElabD ()

1380−resolveTC = resTC' []

1414+resolveTC def mvok depth top fn ist

1381−

1415+ = do hs <- get_holes

1416+ resTC' [] def hs depth top fn ist

1417+

1382−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1418+resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1383−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1419+resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1384−resTC' tcs defaultOn depth topg fn ist

1420+resTC' tcs defaultOn topholes depth topg fn ist

1385− = do compute

1421+ = do compute

1386− g <- goal

1422+ g <- goal

1423+ let argsok = tcArgsOK g topholes

1424+-- trace (show (g,hs,argsok,topholes)) $

1425+ if not argsok -- && not mvok)

1426+ then lift $ tfail $ CantResolve True topg

1427+ else do

1387 ptm <- get_term

1428 ptm <- get_term

1388 ulog <- getUnifyLog

1429 ulog <- getUnifyLog

1389 hs <- get_holes

1430 hs <- get_holes

@@ -1400,6 +1441,31 @@ resTC' tcs defaultOn depth topg fn ist

1400 let depth' = if scopeOnly then 2 else depth

1441 let depth' = if scopeOnly then 2 else depth

1401 blunderbuss t depth' stk (stk ++ insts)) True

1442 blunderbuss t depth' stk (stk ++ insts)) True

1402 where

1443 where

1444+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1445+ = True

1446+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1447+ = let (f, as) = unApply ty in

1448+ case f of

1449+ P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1450+ Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1451+ Nothing -> not $ any (isMeta hs) as

1452+ _ -> not $ any (isMeta hs) as

1453+

1454+ tcDetArgsOK i ds hs (x : xs)

1455+ | i `elem` ds = not (isMeta hs x) && tcDetArgsOK (i + 1) ds hs xs

1456+ | otherwise = tcDetArgsOK (i + 1) ds hs xs

1457+ tcDetArgsOK _ _ _ [] = True

1458+

1459+ isMeta :: [Name] -> Term -> Bool

1460+ isMeta ns (P _ n _) = n `elem` ns

1461+ isMeta _ _ = False

1462+

1463+ notHole hs (P _ n _, c)

1464+ | (P _ cn _, _) <- unApply c,

1465+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1466+ | Constant _ <- c = not (n `elem` hs)

1467+ notHole _ _ = True

1468+

1403 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1469 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1404 | otherwise = (fail "Can't resolve", show n)

1470 | otherwise = (fail "Can't resolve", show n)

1405

1471

@@ -1427,10 +1493,13 @@ resTC' tcs defaultOn depth topg fn ist

1427

1493

1428 blunderbuss t d stk [] = do -- c <- get_env

1494 blunderbuss t d stk [] = do -- c <- get_env

1429 -- ps <- get_probs

1495 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1496+ lift $ tfail $ CantResolve False topg

1431 blunderbuss t d stk (n:ns)

1497 blunderbuss t d stk (n:ns)

1432 | n /= fn && (n `elem` stk || tcname n)

1498 | n /= fn && (n `elem` stk || tcname n)

1499+ = tryCatch (resolve n d)

1500+ (\e -> case e of

1501+ CantResolve True _ -> lift $ tfail e

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1502+ _ -> blunderbuss t d stk ns)

1434 | otherwise = blunderbuss t d stk ns

1503 | otherwise = blunderbuss t d stk ns

1435

1504

1436 resolve n depth

1505 resolve n depth

@@ -1459,7 +1528,7 @@ resTC' tcs defaultOn depth topg fn ist

1459 let got = fst (unApply t)

1528 let got = fst (unApply t)

1460 let depth' = if tc' `elem` tcs

1529 let depth' = if tc' `elem` tcs

1461 then depth - 1 else depth

1530 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1531+ resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

1463 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1532 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1464 -- if there's any arguments left, we've failed to resolve

1533 -- if there's any arguments left, we've failed to resolve

1465 hs <- get_holes

1534 hs <- get_holes

@@ -1505,11 +1574,17 @@ case_ ind autoSolve ist fn tm = do

1505 else casetac (forget val)

1574 else casetac (forget val)

1506 when autoSolve solveAll

1575 when autoSolve solveAll

1507

1576

1577+tacN :: String -> Name

1578+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1579+

1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1580+runTactical :: FC -> Env -> Term -> ElabD ()

1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1581+runTactical fc env tm = do tm' <- eval tm

1582+ runTacTm tm'

1583+ return ()

1510 where

1584 where

1585+ eval tm = do ctxt <- get_context

1511− eval = normaliseAll ctxt env . finalise

1586+ return $ normaliseAll ctxt env (finalise tm)

1512− tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1587+

1513 returnUnit = fmap fst $ get_type_val (Var unitCon)

1588 returnUnit = fmap fst $ get_type_val (Var unitCon)

1514

1589

1515 -- | Do a step in the reflected elaborator monad. The input is the

1590 -- | Do a step in the reflected elaborator monad. The input is the

@@ -1547,26 +1622,31 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1547 = do env <- get_env

1622 = do env <- get_env

1548 fmap fst . get_type_val $ reflectEnv env

1623 fmap fst . get_type_val $ reflectEnv env

1549 | n == tacN "prim__Fail", [_a, errs] <- args

1624 | n == tacN "prim__Fail", [_a, errs] <- args

1625+ = do errs' <- eval errs

1550− = do parts <- reifyReportParts (eval errs)

1626+ parts <- reifyReportParts errs'

1551 lift . tfail $ ReflectionError [parts] (Msg "")

1627 lift . tfail $ ReflectionError [parts] (Msg "")

1552 | n == tacN "prim__PureTactical", [_a, tm] <- args

1628 | n == tacN "prim__PureTactical", [_a, tm] <- args

1553 = return tm

1629 = return tm

1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1630 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1555− = do let first' = eval first

1631+ = do first' <- eval first

1556 res <- runTacTm first'

1632 res <- runTacTm first'

1557− let next = eval (App andThen res)

1633+ next <- eval (App andThen res)

1558 runTacTm next

1634 runTacTm next

1559 | n == tacN "prim__Try", [_a, first, alt] <- args

1635 | n == tacN "prim__Try", [_a, first, alt] <- args

1560− = do let first' = eval first

1636+ = do first' <- eval first

1561− let alt' = eval alt

1637+ alt' <- eval alt

1562 try' (runTacTm first') (runTacTm alt') True

1638 try' (runTacTm first') (runTacTm alt') True

1563 | n == tacN "prim__Fill", [raw] <- args

1639 | n == tacN "prim__Fill", [raw] <- args

1564 = do raw' <- reifyRaw raw

1640 = do raw' <- reifyRaw raw

1565 apply raw' []

1641 apply raw' []

1566 returnUnit

1642 returnUnit

1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

1643+ | n == tacN "prim__Gensym", [hint] <- args

1644+ = do hintStr <- eval hint

1645+ case hintStr of

1646+ Constant (Str h) -> do

1568− = do n <- getNameFrom (sMN 0 hint)

1647+ n <- getNameFrom (sMN 0 h)

1569− fmap fst $ get_type_val (reflectName n)

1648+ fmap fst $ get_type_val (reflectName n)

1649+ _ -> fail "no hint"

1570 | n == tacN "prim__Claim", [n, ty] <- args

1650 | n == tacN "prim__Claim", [n, ty] <- args

1571 = do n' <- reifyTTName n

1651 = do n' <- reifyTTName n

1572 ty' <- reifyRaw ty

1652 ty' <- reifyRaw ty

@@ -1596,6 +1676,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1596 Just name -> fmap Just $ reifyTTName name

1676 Just name -> fmap Just $ reifyTTName name

1597 intro n

1677 intro n

1598 returnUnit

1678 returnUnit

1679+ | n == tacN "prim__DeclareType", [decl] <- args

1680+ = do (RDeclare n args res) <- reifyTyDecl decl

1681+ ctxt <- get_context

1682+ let mkPi arg res = RBind (argName arg)

1683+ (Pi Nothing (argTy arg) (RUType AllTypes))

1684+ res

1685+ rty = foldr mkPi res args

1686+ (checked, ty') <- lift $ check ctxt [] rty

1687+ case normaliseAll ctxt [] (finalise ty') of

1688+ TType _ -> lift . tfail . InternalMsg $

1689+ show checked ++ " is not a type: it's " ++ show ty'

1690+ _ -> return ()

1691+ case lookupDefExact n ctxt of

1692+ Just _ -> lift . tfail . InternalMsg $

1693+ show n ++ " is already defined."

1694+ Nothing -> return ()

1695+ let decl = TyDecl Ref checked

1696+ ctxt' = addCtxtDef n decl ctxt

1697+ set_context ctxt'

1698+ updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :

1699+ new_tyDecls e }

1700+ aux <- getAux

1701+ returnUnit

1599 | n == tacN "prim__Debug", [ty, msg] <- args

1702 | n == tacN "prim__Debug", [ty, msg] <- args

1600 = do let msg' = fromTTMaybe msg

1703 = do let msg' = fromTTMaybe msg

1601 case msg' of

1704 case msg' of

@@ -1850,6 +1953,7 @@ runTac autoSolve ist perhapsFC fn tac

1850 Just fc ->

1953 Just fc ->

1851 do fill $ reflectFC fc

1954 do fill $ reflectFC fc

1852 solve

1955 solve

1956+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

1853 runT x = fail $ "Not implemented " ++ show x

1957 runT x = fail $ "Not implemented " ++ show x

1854

1958

1855 runReflected t = do t' <- reify ist t

1959 runReflected t = do t' <- reify ist t

@@ -2361,7 +2465,7 @@ reflectTTQuote unq (P nt n t)

2361reflectTTQuote unq (V n)

2465reflectTTQuote unq (V n)

2362 = reflCall "V" [RConstant (I n)]

2466 = reflCall "V" [RConstant (I n)]

2363reflectTTQuote unq (Bind n b x)

2467reflectTTQuote unq (Bind n b x)

2364− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]

2468+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2365reflectTTQuote unq (App f x)

2469reflectTTQuote unq (App f x)

2366 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2367reflectTTQuote unq (Constant c)

2471reflectTTQuote unq (Constant c)

@@ -2378,7 +2482,7 @@ reflectRawQuote unq (Var n)

2378 | n `elem` unq = Var n

2482 | n `elem` unq = Var n

2379 | otherwise = reflCall "Var" [reflectName n]

2483 | otherwise = reflCall "Var" [reflectName n]

2380reflectRawQuote unq (RBind n b r) =

2484reflectRawQuote unq (RBind n b r) =

2381− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]

2485+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2382reflectRawQuote unq (RApp f x) =

2486reflectRawQuote unq (RApp f x) =

2383 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2384reflectRawQuote unq RType = Var (reflm "RType")

2488reflectRawQuote unq RType = Var (reflm "RType")

@@ -2436,27 +2540,27 @@ reflectNameQuotePattern _ -- for all other names, match any

2436 solve

2540 solve

2437

2541

2438reflectBinder :: Binder Term -> Raw

2542reflectBinder :: Binder Term -> Raw

2439−reflectBinder = reflectBinderQuote reflectTTQuote []

2543+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2440−

2544+

2441−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2545+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2442−reflectBinderQuote q unq (Lam t)

2546+reflectBinderQuote q ty unq (Lam t)

2443− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2547+ = reflCall "Lam" [Var ty, q unq t]

2444−reflectBinderQuote q unq (Pi _ t k)

2548+reflectBinderQuote q ty unq (Pi _ t k)

2445− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2549+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2446−reflectBinderQuote q unq (Let x y)

2550+reflectBinderQuote q ty unq (Let x y)

2447− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2551+ = reflCall "Let" [Var ty, q unq x, q unq y]

2448−reflectBinderQuote q unq (NLet x y)

2552+reflectBinderQuote q ty unq (NLet x y)

2449− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2450−reflectBinderQuote q unq (Hole t)

2554+reflectBinderQuote q ty unq (Hole t)

2451− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2555+ = reflCall "Hole" [Var ty, q unq t]

2452−reflectBinderQuote q unq (GHole _ t)

2556+reflectBinderQuote q ty unq (GHole _ t)

2453− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2557+ = reflCall "GHole" [Var ty, q unq t]

2454−reflectBinderQuote q unq (Guess x y)

2558+reflectBinderQuote q ty unq (Guess x y)

2455− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2456−reflectBinderQuote q unq (PVar t)

2560+reflectBinderQuote q ty unq (PVar t)

2457− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2561+ = reflCall "PVar" [Var ty, q unq t]

2458−reflectBinderQuote q unq (PVTy t)

2562+reflectBinderQuote q ty unq (PVTy t)

2459− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2563+ = reflCall "PVTy" [Var ty, q unq t]

2460

2564

2461mkList :: Raw -> [Raw] -> Raw

2565mkList :: Raw -> [Raw] -> Raw

2462mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2603,11 +2707,14 @@ reflectErr (NotInjective t1 t2 t3) =

2603 , reflect t2

2707 , reflect t2

2604 , reflect t3

2708 , reflect t3

2605 ]

2709 ]

2606−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2710+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2607reflectErr (CantResolveAlts ss) =

2711reflectErr (CantResolveAlts ss) =

2608 raw_apply (Var $ reflErrName "CantResolveAlts")

2712 raw_apply (Var $ reflErrName "CantResolveAlts")

2609 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2713 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2610reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2714reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2715+reflectErr (NoEliminator str t)

2716+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2717+ reflect t]

2611reflectErr UniverseError = Var $ reflErrName "UniverseError"

2718reflectErr UniverseError = Var $ reflErrName "UniverseError"

2612reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2719reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2613reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2720reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2748,6 +2855,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

2748 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2855 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2749reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2856reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2750

2857

2858+reifyTyDecl :: Term -> ElabD RTyDecl

2859+reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2860+ | n == tacN "Declare" =

2861+ do tyN' <- reifyTTName tyN

2862+ args' <- case unList args of

2863+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2864+ Just xs -> mapM reifyRArg xs

2865+ ret' <- reifyRaw ret

2866+ return $ RDeclare tyN' args' ret'

2867+ where reifyRArg :: Term -> ElabD RArg

2868+ reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2869+ | n == tacN "Explicit" = liftM2 RExplicit

2870+ (reifyTTName argN)

2871+ (reifyRaw argTy)

2872+ | n == tacN "Implicit" = liftM2 RImplicit

2873+ (reifyTTName argN)

2874+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2875+ (reifyTTName argN)

2876+ (reifyRaw argTy)

2877+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2878+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2879+

2751envTupleType :: Raw

2880envTupleType :: Raw

2752envTupleType

2881envTupleType

2753 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2882 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/IBC.hs+12−8

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

@@ -365,7 +365,7 @@ pClasses cs = mapM_ (\ (n, c) ->

365 -- Don't lose instances from previous IBCs, which

366 -- could have loaded in any order

367 let is = case lookupCtxtExact n (idris_classes i) of

368− Just (CI _ _ _ _ _ ins) -> ins

368+ Just (CI _ _ _ _ _ ins _) -> ins

369 _ -> []

370 let c' = c { class_instances =

371 class_instances c ++ is }

@@ -1238,7 +1238,7 @@ instance (Binary t) => Binary (PDecl' t) where

1238 put x7

1239 put x8

1240 put x9

1241− PClass x1 x2 x3 x4 x5 x6 x7 x8

1241+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

1242 -> do putWord8 7

1243 put x1

1244 put x2

@@ -1248,6 +1248,7 @@ instance (Binary t) => Binary (PDecl' t) where

1248 put x6

1249 put x7

1250 put x8

1251+ put x9

1251 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252 do putWord8 8

1253 do putWord8 8

1253 put x1

1254 put x1

@@ -1346,7 +1347,8 @@ instance (Binary t) => Binary (PDecl' t) where

1346 x6 <- get

1347 x6 <- get

1347 x7 <- get

1348 x7 <- get

1348 x8 <- get

1349 x8 <- get

1350+ x9 <- get

1349− return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1351+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

1350 8 -> do x1 <- get

1352 8 -> do x1 <- get

1351 x2 <- get

1353 x2 <- get

1352 x3 <- get

1354 x3 <- get

@@ -1418,7 +1420,7 @@ instance Binary Using where

1418 _ -> error "Corrupted binary data for Using"

1420 _ -> error "Corrupted binary data for Using"

1419

1421

1420instance Binary SyntaxInfo where

1422instance Binary SyntaxInfo where

1421− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1423+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

1422 = do put x1

1424 = do put x1

1423 put x2

1425 put x2

1424 put x3

1426 put x3

@@ -1434,7 +1436,7 @@ instance Binary SyntaxInfo where

1434 x5 <- get

1436 x5 <- get

1435 x6 <- get

1437 x6 <- get

1436 x7 <- get

1438 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)

1438

1440

1439instance (Binary t) => Binary (PClause' t) where

1441instance (Binary t) => Binary (PClause' t) where

1440 put x

1442 put x

@@ -2071,19 +2073,21 @@ instance (Binary t) => Binary (PArg' t) where

2071

2073

2072

2074

2073instance Binary ClassInfo where

2075instance Binary ClassInfo where

2074− put (CI x1 x2 x3 x4 x5 _)

2076+ put (CI x1 x2 x3 x4 x5 _ x6)

2075 = do put x1

2077 = do put x1

2076 put x2

2078 put x2

2077 put x3

2079 put x3

2078 put x4

2080 put x4

2079 put x5

2081 put x5

2082+ put x6

2080 get

2083 get

2081 = do x1 <- get

2084 = do x1 <- get

2082 x2 <- get

2085 x2 <- get

2083 x3 <- get

2086 x3 <- get

2084 x4 <- get

2087 x4 <- get

2085 x5 <- get

2088 x5 <- get

2089+ x6 <- get

2086− return (CI x1 x2 x3 x4 x5 [])

2090+ return (CI x1 x2 x3 x4 x5 [] x6)

2087

2091

2088instance Binary OptInfo where

2092instance Binary OptInfo where

2089 put (Optimise x1 x2)

2093 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

@@ -585,8 +585,8 @@ collect (c@(PClauses _ o _ _) : ds)

585collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

586collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588−collect (PClass doc f s cs n ps pdocs ds : ds')

588+collect (PClass doc f s cs n ps pdocs fds ds : ds')

589− = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

589+ = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

590collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592collect (d : ds) = d : collect ds

src/Idris/Parser.hs+5−1

@@ -612,11 +612,15 @@ class_ syn = do (doc, argDocs, acc)

612 n_in <- fnName

613 let n = expandNS syn n_in

614 cs <- many carg

615+ fds <- option (map fst cs) fundeps

615 ds <- option [] (classBlock syn)

616 ds <- option [] (classBlock syn)

616 accData acc n (concatMap declared ds)

617 accData acc n (concatMap declared ds)

617− return [PClass doc syn fc cons n cs argDocs ds]

618+ return [PClass doc syn fc cons n cs argDocs fds ds]

618 <?> "type-class declaration"

619 <?> "type-class declaration"

619 where

620 where

621+ fundeps :: IdrisParser [Name]

622+ fundeps = do lchar '|'; sepBy name (lchar ',')

623+

620 carg :: IdrisParser (Name, PTerm)

624 carg :: IdrisParser (Name, PTerm)

621 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

625 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

622 return (i, ty)

626 return (i, ty)

src/Idris/REPL.hs+1−1

@@ -773,7 +773,7 @@ process fn (NewDefn decls) = do

773 getName (PTy docs argdocs syn fc opts name ty) = Just name

774 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

775 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

776− getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name

776+ getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

777 getName _ = Nothing

778 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

779 getClauseName (PClause fc name whole with rhs whereBlock) = name

src/Idris/Reflection.hsnew file+18

@@ -0,0 +1,18 @@

1+{-|

2+Handy tools for doing reflection.

3+-}

4+module Idris.Reflection where

5+

6+import Idris.Core.TT

7+import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))

8+

9+data RArg = RExplicit { argName :: Name, argTy :: Raw }

10+ | RImplicit { argName :: Name, argTy :: Raw }

11+ | RConstraint { argName :: Name, argTy :: Raw }

12+

13+data RTyDecl = RDeclare Name [RArg] Raw

14+

15+rArgToPArg :: RArg -> PArg

16+rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

17+rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

18+rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

src/Idris/TypeSearch.hs+1−1

@@ -46,7 +46,7 @@ searchByType pkgs pterm = do

46 mapM_ loadPkgIndex pkgs

47 pterm' <- addUsingConstraints syn emptyFC pterm

48 pterm'' <- implicit toplevel syn name pterm'

49− let pterm''' = addImpl i pterm''

49+ let pterm''' = addImpl [] i pterm''

50 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

51 let names = searchUsing searchPred i ty

52 let names' = take numLimit names

test/basic002/test006.idr+1−1

@@ -18,7 +18,7 @@ natToBin k with (parity k)

18 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

19

20main : IO ()

21−main = do print (natToBin 42)

21+main = do printLn (natToBin 42)

22

23---------- Proofs ----------

24

test/basic003/test027.idr+3−3

@@ -19,7 +19,7 @@ using (Ord a, Num n)

19 mprod (x :: xs) = x * mprod xs

20

21main : IO ()

22−main = do print $ isort [1,5,3,5,1,9,8]

22+main = do printLn $ isort [1,5,3,5,1,9,8]

23− print $ msum [1..10]

23+ printLn $ msum [1..10]

24− print $ mprod [1..10]

24+ printLn $ mprod [1..10]

25

test/basic004/test016.idr+1−1

@@ -13,5 +13,5 @@ take (S n) (x :: xs) = x :: take n xs

13take n [] = []

14

15main : IO ()

16−main = do print (take 10 (Main.countFrom 10))

16+main = do printLn (take 10 (Main.countFrom 10))

17

test/basic005/test019.lidr+1−1

@@ -14,5 +14,5 @@

14> | False = ifFalse x

15

16> main : IO ()

17−> main = print (test ((S 4) ==) 5 Oh)

17+> main = printLn (test ((S 4) ==) 5 Oh)

18

test/basic006/test020.idr+2−2

@@ -21,7 +21,7 @@ test : Integer -> String

21test x = "Number " ++ x

22

23main : IO ()

24−main = do print (foo [1,2,3])

24+main = do printLn (foo [1,2,3])

25− print (test 42)

25+ printLn (test 42)

26

27

test/basic006/test020a.idr+1−1

@@ -16,5 +16,5 @@ foo : Vect n a -> List a

16foo xs = reverse xs

17

18main : IO ()

19−main = print (foo [1,2,3])

19+main = printLn (foo [1,2,3])

20

test/basic007/test033.idr+1−1

@@ -1,4 +1,4 @@

1module Main

2

3main : IO ()

4−main = nullPtr null >>= print

4+main = nullPtr null >>= printLn

test/basic011/basic011.idr+10−10

@@ -3,14 +3,14 @@ module Main

3import Data.Hash

4

5main : IO ()

6−main = do print $ hash (the Bits8 3)

6+main = do printLn $ hash (the Bits8 3)

7− print $ hash (the (List Bits8) [3])

7+ printLn $ hash (the (List Bits8) [3])

8− print $ hash "hello world"

8+ printLn $ hash "hello world"

9− print $ hash 'a'

9+ printLn $ hash 'a'

10− print $ hash (the Bits8 3)

10+ printLn $ hash (the Bits8 3)

11− print $ hash (the Bits16 3)

11+ printLn $ hash (the Bits16 3)

12− print $ hash (the Bits32 3)

12+ printLn $ hash (the Bits32 3)

13− print $ hash (the Bits64 3)

13+ printLn $ hash (the Bits64 3)

14− print $ hash (the Int 3)

14+ printLn $ hash (the Int 3)

15− print $ hash (the Integer 3)

15+ printLn $ hash (the Integer 3)

16

test/basic012/basic012.idr+5−4

@@ -1,7 +1,7 @@

1import Data.Vect

2import Control.Monad.State

3import Control.Monad.Identity

4−

4+

5VThing : Type

6VThing = {n : Nat} -> Vect n Int -> Int

7

@@ -31,7 +31,8 @@ testfoo3 xs = foo 42 xs (bar 10)

31AnyST : Type -> Type -> Type

32AnyST s a = {m : _} -> Monad m => StateT s m a

33

34−foost: AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

35foost = do x <- get

36foost = do x <- get

36 put x

37 put x

37

38

@@ -52,11 +53,11 @@ tupleId f (a, b) = (f a, f b)

52

53

53AppendType : Type

54AppendType : Type

54AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55−

56+

56append : AppendType

57append : AppendType

57append [] ys = ys

58append [] ys = ys

58append (x :: xs) ys = x :: append xs ys

59append (x :: xs) ys = x :: append xs ys

59

60

60main : IO ()

61main : IO ()

61main = do putStrLn (baz 42)

62main = do putStrLn (baz 42)

62− print (append [1,2,3] [4,5,6])

63+ printLn (append [1,2,3] [4,5,6])

test/dsl001/test001.idr+2−2

@@ -96,8 +96,8 @@ testEnv : Int -> Env [TyInt,TyInt]

96testEnv x = [x,x]

97

98main : IO ()

99−main = do { print testFac

99+main = do { printLn testFac

100− print test }

100+ printLn test }

101

102

103

test/effects002/test025.idr+1−1

@@ -30,6 +30,6 @@ testMemory = do Src :- allocate 5

30

31main : IO ()

32main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

33− (\err => print err) (\ok => print ok)

33+ (\err => printLn err) (\ok => printLn ok)

34

35

test/io002/test008.idr+1−1

@@ -22,7 +22,7 @@ main = do (a, b) <- ioVals

22 let x = "bar"

23 putStrLn (show (getVal x 7 testlist))

24 let ((y, z) :: _) = testlist

25− print z

25+ printLn z

26 case lookup x testlist of

27 Just v => putStrLn (show v)

28 Nothing => putStrLn "Not there!"

test/io003/test018a.idr+1−1

@@ -27,7 +27,7 @@ mainProc = do mainID <- myID

27

28repeatIO : Int -> IO ()

29repeatIO 0 = return ()

30−repeatIO n = do print n

30+repeatIO n = do printLn n

31 run mainProc

32 repeatIO (n - 1)

33

test/primitives001/test005.idr+6−6

@@ -7,9 +7,9 @@ tlist : List Int

7tlist = [1, 2, 3, 4, 5]

8

9main : IO ()

10−main = do print (abs (-8))

10+main = do printLn (abs (-8))

11− print (abs (S Z))

11+ printLn (abs (S Z))

12− print (span isAlpha tstr)

12+ printLn (span isAlpha tstr)

13− print (break isDigit tstr)

13+ printLn (break isDigit tstr)

14− print (span (\x => x < 3) tlist)

14+ printLn (span (\x => x < 3) tlist)

15− print (break (\x => x > 2) tlist)

15+ printLn (break (\x => x > 2) tlist)

test/proof003/test015.idr+3−3

@@ -72,10 +72,10 @@ readNum = do putStr "Enter a number:"

72

73main : IO ()

74main = do let Just bin1 = natToBin 8 42

75− print bin1

75+ printLn bin1

76 let Just bin2 = natToBin 8 89

77− print bin2

77+ printLn bin2

78− print (adc bin1 bin2 b0)

78+ printLn (adc bin1 bin2 b0)

79

80

81

test/records001/test011.idr+5−5

@@ -20,9 +20,9 @@ person = MkPerson "Fred" 30

20main : IO ()

21main = do let x = record { name = "foo",

22 more_things = reverse ["a","b"] } testFoo

23− print $ name x

23+ printLn $ name x

24− print $ name person

24+ printLn $ name person

25− print $ things x

25+ printLn $ things x

26− print $ more_things x

26+ printLn $ more_things x

27− print $ age (record { age = 25 } person)

27+ printLn $ age (record { age = 25 } person)

28

test/records003/records003.idr+6−6

@@ -38,10 +38,10 @@ test : Meeting 2015

38test = next_year idm_gbg

39

40main : IO ()

41−main = do print (record { event->organiser->name } test)

41+main = do printLn (record { event->organiser->name } test)

42− print (record { event->organiser->age } test)

42+ printLn (record { event->organiser->age } test)

43− print (record { event->organiser->age } idm_gbg)

43+ printLn (record { event->organiser->age } idm_gbg)

44− print (record { organiser->age } test)

44+ printLn (record { organiser->age } test)

45− print (record { organiser->age } idm_gbg)

45+ printLn (record { organiser->age } idm_gbg)

46− print (record { year } idm_gbg)

46+ printLn (record { year } idm_gbg)

47

test/reg002/reg012.idr+1−1

@@ -30,4 +30,4 @@ swap (x :: Nil) = x :: Nil

30swap (x :: y :: xs) = (y :: x :: (swap xs))

31

32main : IO ()

33−main = print (swap [1,2,3,4,5])

33+main = printLn (swap [1,2,3,4,5])

test/reg004/reg004.idr+1−1

@@ -13,4 +13,4 @@ h True = r2 where

13 r2 = r

14

15main : IO ()

16−main = do print (h True); print (h False)

16+main = do printLn (h True); printLn (h False)

test/reg013/reg013.idr+3−3

@@ -2,7 +2,7 @@ module Main

2

3main : IO ()

4main = do

5− print $ prim_lenString "hallo"

5+ printLn $ prim_lenString "hallo"

6− print $ prim_lenString "1"

6+ printLn $ prim_lenString "1"

7− print $ prim_lenString ""

7+ printLn $ prim_lenString ""

8

test/reg016/reg016.idr+6−6

@@ -1,11 +1,11 @@

1module Main

2

3main : IO ()

4−main = do print $ the Integer 429496729500000000000000

4+main = do printLn $ the Integer 429496729500000000000000

5−-- print $ the Integer 4294967296

5+-- printLn $ the Integer 4294967296

6−-- print $ the Integer 4294967297

6+-- printLn $ the Integer 4294967297

7−-- print $ the Int 4294967295

7+-- printLn $ the Int 4294967295

8−-- print $ the Int 4294967296

8+-- printLn $ the Int 4294967296

9−-- print $ the Int 4294967297

9+-- printLn $ the Int 4294967297

10

11

test/reg017/reg017.idr+1−1

@@ -10,4 +10,4 @@ foo : { t : Type } ->

10foo {t} a {prfA = p} b c {prfBC} = b

11

12main : IO ()

13−main = print $ foo 3 4 4

13+main = printLn $ foo 3 4 4

test/reg018/reg018d.idr+1−1

@@ -12,4 +12,4 @@ pull {n=S _} (FS n) (x :: xs) =

12 (v, x::vs)

13

14main : IO ()

15−main = print (pull FZ [0, 1, 2])

15+main = printLn (pull FZ [0, 1, 2])

test/reg027/reg027.idr+1−1

@@ -27,6 +27,6 @@ foo = do val <- dbl

27 \x => show val

28

29main : IO ()

30−main = do print dbl

30+main = do printLn dbl

31 putStrLn (foo 3)

32

test/reg029/reg029.idr+2−2

@@ -7,5 +7,5 @@ import System

7

8main : IO ()

9main = do

10− print !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

10+ printLn !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11− print !(getEnv "IDRIS_REG029_EXISTENT_VAR")

11+ printLn !(getEnv "IDRIS_REG029_EXISTENT_VAR")

test/reg031/reg031.idr+1−1

@@ -1,7 +1,7 @@

1module Main

2

3main : IO ()

4−main = print . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

4+main = printLn . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

5 where

6 -- make the values positive if the backend has signed chars

7 val : Char -> Int

test/reg040/reg040.idr+1−1

@@ -4,4 +4,4 @@ io : IO Int

4io = return 42

5

6main : IO ()

7−main = print $ unsafePerformIO io

7+main = printLn $ unsafePerformIO io

test/reg042/reg042.idr+1−1

@@ -21,4 +21,4 @@ g (C x y z) = x + y

21-- Here, we'd apply the not-a-function to the erased argument 4,

22-- which would make the program go wrong.

23main : IO ()

24−main = print $ g (proj 3 f 4)

24+main = printLn $ g (proj 3 f 4)

test/reg045/reg045.idr+1−1

@@ -15,5 +15,5 @@ foo : ListZ Nat

15foo = (1 :: 2 :: 3 :: Nil)

16

17main : IO ()

18−main = print foo

18+main = printLn foo

19

test/reg052/reg052.idr+1−1

@@ -5,4 +5,4 @@ impure_int : IO Int

5impure_int = return 41

6

7main : IO ()

8−main = impure_int >>= impure_op . prim__zextInt_B64 >>= print

8+main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/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)

36 Var : (i : Fin n) -> Tm ctxt (index i ctxt)

37 Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

38 App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'

39− ||| A term that makes the program halt and print where it halted

39+ ||| A term that makes the program halt and printLn where it halted

40 Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

41

42 data Env : Vect n Ty -> Type where

@@ -83,11 +83,11 @@ testTerm4 = App testTerm3 MkU

83namespace Main

84 main : IO ()

85 main = do putStrLn "Testing using definition"

86− print fromRHS

86+ printLn fromRHS

87 putStrLn "Testing using inline tactics"

88− print fromProofScript

88+ printLn fromProofScript

89 putStrLn "Testing using metavariable with later definition"

90− print fromMetavar

90+ printLn fromMetavar

91 putStrLn "-----------------------"

92 sequence_ $ with List [ exec testTerm1

93 , exec testTerm2

test/sugar001/test007.idr+4−4

@@ -35,7 +35,7 @@ runEval env e with (eval e) {

35}

36

37main : IO ()

38−main = do print [| (\x => x *2) (Just 4) |]

38+main = do printLn [| (\x => x *2) (Just 4) |]

39− print [| plus (Just 4) (Just 5) |]

39+ printLn [| plus (Just 4) (Just 5) |]

40− print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

40+ printLn (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41− print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41+ printLn (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

test/sugar004/sugar004.idr+1−1

@@ -9,7 +9,7 @@ foo x = let Just x' = x | Nothing => 100 in x'

9main : IO ()

10main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

11 | (x :: y :: _) => putStrLn "Too many arguments!"

12− print (foo (Just (cast a)))

12+ printLn (foo (Just (cast a)))

13

14{-

15

test/sugar005/As.idr+9−9

@@ -24,13 +24,13 @@ same _ _ = Nothing

24

25namespace Main

26 main : IO ()

27− main = do print $ isS 0

27+ main = do printLn $ isS 0

28− print $ isS 1

28+ printLn $ isS 1

29− print $ hasS [0,0,0]

29+ printLn $ hasS [0,0,0]

30− print $ hasS [0,1,2]

30+ printLn $ hasS [0,1,2]

31− print $ isSS 5

31+ printLn $ isSS 5

32− print $ isSS 0

32+ printLn $ isSS 0

33− print $ same 1 1

33+ printLn $ same 1 1

34− print $ same 0 0

34+ printLn $ same 0 0

35− print $ same 1 0

35+ printLn $ same 1 0

36

test/tactics001/Tactics.idr+14

@@ -2,6 +2,9 @@ module Tactics

2

3import Language.Reflection.Tactical

4

5+import Data.Vect

6+

7+

5%default total

8%default total

6

9

7-- Test that basic proofs with new-style tactics work

10-- Test that basic proofs with new-style tactics work

@@ -25,3 +28,14 @@ plusSuccRightSuccNew (S j) k =

25 %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

28 %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

26 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

29 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

27 solve)

30 solve)

31+

32+-- Test that side effects in new tactics work

33+

34+mkDecl : ()

35+mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

36+ [Implicit (UN "z") `(Nat)]

37+ `(Vect ~(Var (UN "z")) ())

38+ fill `(() : ())

39+ solve)

40+

41+repUnit = pure ()

test/totality004/totality004.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

21countStream x = x :: countStream (x + 1)

22

23main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

25

test/totality004/totality004a.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

21countStream x = x :: countStream (x + 1)

22

23main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

25

test/totality005/totality005.idr+1−1

@@ -7,4 +7,4 @@ fib : Stream Nat

7fib = 0 :: zipWithS (+) fib (1 :: fib)

8

9partial main : IO ()

10−main = print (take 15 fib)

10+main = printLn (take 15 fib)

test/tutorial002/tutorial002.idr+1−1

@@ -34,7 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

34main : IO ()

35main = do putStr "Enter a number: "

36 x <- getLine

37− print (natToBin (fromInteger (cast x)))

37+ printLn (natToBin (fromInteger (cast x)))

38

39---------- Proofs ----------

40