bbbe880 · Idris-dev · git.iko.soy

CHANGELOG+10−1

compare with master

unifiedsplit

@@ -34,7 +34,16 @@ New in 0.9.17:

34 command :elaborate-term for serialized terms.

35* Records has a new syntax based on fields rather than constructors.

36* Records can now be coinductive.

37−

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

38+ aligned, semantically.

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

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

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

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

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

44+ are checked when checking for overlapping instances.

45+* Arguments to class instances are now checked for injectivity.

46+ Unification assumes this, so we need to check when instances are defined.

38

47

39New in 0.9.16:

48New in 0.9.16:

40--------------

49--------------

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

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

289 test/reg058/run

290 test/reg058/*.idr

291 test/reg058/expected

292+ test/reg059/run

293+ test/reg059/*.idr

294+ test/reg059/expected

292

295

293 test/basic001/run

296 test/basic001/run

294 test/basic001/*.idr

297 test/basic001/*.idr

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

658 Default: False

661 Default: False

659 manual: True

662 manual: True

660

663

664+Flag execonly

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

666+ Default: False

667+ manual: True

668+

661Library

669Library

662 hs-source-dirs: src

670 hs-source-dirs: src

663 Exposed-modules:

671 Exposed-modules:

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

725 , Idris.ProofSearch

733 , Idris.ProofSearch

726 , Idris.Prover

734 , Idris.Prover

727 , Idris.Providers

735 , Idris.Providers

736+ , Idris.Reflection

728 , Idris.REPL

737 , Idris.REPL

729 , Idris.REPLParser

738 , Idris.REPLParser

730 , Idris.Transforms

739 , 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

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

56

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

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

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

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

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

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

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

61 return (a, f' w)

62 return (a, f' w)

62

63

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

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

146isEmptySizeZero Empty p = Refl

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

148

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

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

150emptyHeapValid = Refl

151

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

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

182 does seem to work correctly!

183main : IO ()

184main = do

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

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

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

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

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

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

188 return ()

189-}

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

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

36 eq (f a) (f b)

37

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

39−minimum x y with (order x y)

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

40 | Left _ = x

41 | Right _ = y

42

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

44−maximum x y with (order x y)

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

45 | Left _ = y

46 | Right _ = x

47

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

103decideLTE Z y = Yes LTEZero

104decideLTE (S x) Z = No zeroNeverGreater

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

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

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

107 | No _ with (decideLTE x y)

108 | Yes nLTEm = Yes (LTESucc nLTEm)

109 | No nGTm = No (ltesuccinjective nGTm)

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

122instance Ordered Nat LTE where

123 order Z n = Left LTEZero

124 order m Z = Right LTEZero

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

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

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

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

128

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

@@ -270,8 +270,10 @@ instance Show Err where

270 show (NoTypeDecl n) = "NoTypeDecl " ++ show n

271 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

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

273+ show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"

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

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

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

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

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

275 show UniverseError = "UniverseError"

277 show UniverseError = "UniverseError"

276 show ProgramLineComment = "ProgramLineComment"

278 show ProgramLineComment = "ProgramLineComment"

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

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

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

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

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

9

10instance Handler (Exception a) Maybe where

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

14 handle _ (Raise e) k = []

15

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

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

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

18 believe_me (exit 1)

19

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

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

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

39

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

41-- handler can be introduced mid interpretation?

42−

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

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

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

43putStr s = call $ PutStr s

44

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

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

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

48+

45||| Write a character to standard output.

49||| Write a character to standard output.

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

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

47putChar c = call $ PutCh c

51putChar c = call $ PutCh c

48

52

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

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

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

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

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

55+putCharLn c = putStrLn (singleton c)

52

56

53||| Read a string from standard input.

57||| Read a string from standard input.

54getStr : { [STDIO] } Eff String

58getStr : { [STDIO] } Eff String

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

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

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

9

10instance Handler (Exception a) Maybe where

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

14 handle _ (Raise e) k = []

15

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

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

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

18 believe_me (exit 1)

19

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

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

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

39

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

41-- handler can be introduced mid interpretation?

42−

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

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

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

417

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

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

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

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

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

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

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

422

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

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

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

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

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

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

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

427

428instance Quotable TTName TT where

429 quotedTy = `(TTName)

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

@@ -29,8 +29,10 @@ data Err = Msg String

29 | NoTypeDecl TTName

30 | NotInjective TT TT TT

31 | CantResolve TT

32+ | InvalidTCArg TTName TT

32 | CantResolveAlts (List TTName)

33 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34 | IncompleteTerm TT

35+ | NoEliminator String TT

34 | UniverseError

36 | UniverseError

35 | ProgramLineComment

37 | ProgramLineComment

36 | Inaccessible TTName

38 | 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/Applicative.idr−4

@@ -15,10 +15,6 @@ class Functor f => Applicative (f : Type -> Type) where

15 pure : a -> f a

16 (<*>) : f (a -> b) -> f a -> f b

17

18−instance Applicative id where

19− pure a = a

20− f <*> a = f a

21−

22class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

18class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

23 applicativeMap : (x : f a) -> (g : a -> b) ->

19 applicativeMap : (x : f a) -> (g : a -> b) ->

24 map g x = pure g <*> x

20 map g x = pure g <*> x

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

libs/prelude/Prelude/Functor.idr−2

@@ -24,5 +24,3 @@ class Functor f => VerifiedFunctor (f : Type -> Type) where

24 (g1 : a -> b) -> (g2 : b -> c) ->

25 map (g2 . g1) x = (map g2 . map g1) x

26

27−instance Functor id where

28− map f a = f a

libs/prelude/Prelude/Monad.idr−3

@@ -24,9 +24,6 @@ class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

24 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

25 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

26

27−instance Monad id where

28− a >>= f = f a

29−

30||| Also called `join` or mu

27||| Also called `join` or mu

31flatten : Monad m => m (m a) -> m a

28flatten : Monad m => m (m a) -> m a

32flatten a = a >>= id

29flatten a = a >>= id

rts/idris_gc.c+3−14

@@ -112,19 +112,8 @@ void idris_gc(VM* vm) {

112 if (vm->heap.old != NULL)

113 free(vm->heap.old);

114

115− char* newheap = malloc(vm->heap.size);

115+ /* Allocate swap heap. */

116− char* oldheap = vm->heap.heap;

116+ alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, vm->heap.heap);

117−

118− vm->heap.heap = newheap;

119−#ifdef FORCE_ALIGNMENT

120− if (((i_int)(vm->heap.heap)&1) == 1) {

121− vm->heap.next = newheap + 1;

122− } else

123−#endif

124− {

125− vm->heap.next = newheap;

126− }

127− vm->heap.end = newheap + vm->heap.size;

128

117

129 VAL* root;

118 VAL* root;

130

119

@@ -139,6 +128,7 @@ void idris_gc(VM* vm) {

139 msg->msg = copy(vm, msg->msg);

128 msg->msg = copy(vm, msg->msg);

140 }

129 }

141#endif

130#endif

131+

142 vm->ret = copy(vm, vm->ret);

132 vm->ret = copy(vm, vm->ret);

143 vm->reg1 = copy(vm, vm->reg1);

133 vm->reg1 = copy(vm, vm->reg1);

144

134

@@ -150,7 +140,6 @@ void idris_gc(VM* vm) {

150 if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {

140 if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {

151 vm->heap.size += vm->heap.growth;

141 vm->heap.size += vm->heap.growth;

152 }

142 }

153− vm->heap.old = oldheap;

154

143

155 STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)

144 STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)

156 HEAP_CHECK(vm)

145 HEAP_CHECK(vm)

rts/idris_heap.c+6−3

@@ -5,7 +5,9 @@

5#include <stddef.h>

6#include <stdio.h>

7

8+

9+/* Used for initializing the heap. */

8−void alloc_heap(Heap * h, size_t heap_size)

10+void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)

9{

11{

10 char * mem = malloc(heap_size);

12 char * mem = malloc(heap_size);

11 if (mem == NULL) {

13 if (mem == NULL) {

@@ -27,9 +29,9 @@ void alloc_heap(Heap * h, size_t heap_size)

27 h->end = h->heap + heap_size;

29 h->end = h->heap + heap_size;

28

30

29 h->size = heap_size;

31 h->size = heap_size;

30− h->growth = heap_size;

32+ h->growth = growth;

31

33

32− h->old = NULL;

34+ h->old = old;

33}

35}

34

36

35void free_heap(Heap * h) {

37void free_heap(Heap * h) {

@@ -40,6 +42,7 @@ void free_heap(Heap * h) {

40 }

42 }

41}

43}

42

44

45+

43// TODO: more testing

46// TODO: more testing

44/******************** Heap testing ********************************************/

47/******************** Heap testing ********************************************/

45void heap_check_underflow(Heap * heap) {

48void heap_check_underflow(Heap * heap) {

rts/idris_heap.h+1−1

@@ -14,7 +14,7 @@ typedef struct {

14} Heap;

15

16

17−void alloc_heap(Heap * heap, size_t heap_size);

17+void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old);

18void free_heap(Heap * heap);

19

20

rts/idris_rts.c+1−1

@@ -29,7 +29,7 @@ VM* init_vm(int stack_size, size_t heap_size,

29 vm->valstack_base = valstack;

30 vm->stack_max = valstack + stack_size;

31

32− alloc_heap(&(vm->heap), heap_size);

32+ alloc_heap(&(vm->heap), heap_size, heap_size, NULL);

33

34 vm->ret = NULL;

35 vm->reg1 = NULL;

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

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

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

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

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

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

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

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

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

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

1078 = PClass doc info f

1091 = PClass doc info f

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

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

1080 n

1093 n

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

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

1082 pDocs

1095 pDocs

1096+ fds

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

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

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

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

1085 = PInstance doc argDocs info f

1099 = PInstance doc argDocs info f

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

1466

1480

1467-- Add implicit arguments in function calls

1481-- Add implicit arguments in function calls

1468addImplPat :: IState -> PTerm -> PTerm

1482addImplPat :: IState -> PTerm -> PTerm

1469−addImplPat = addImpl' True [] []

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

1470

1484

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

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

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

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

1473

1487

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

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

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

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

1476

1490

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

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

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

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

1494+-- type classes).

1478−addImpl :: IState -> PTerm -> PTerm

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

1479addImpl = addImpl' False [] []

1496addImpl = addImpl' False [] []

1480

1497

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

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

1482-- and *not* inside a PHidden

1499-- and *not* inside a PHidden

1483

1500

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

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

1485−addImpl' inpat env infns ist ptm

1502+addImpl' inpat env infns imp_meths ist ptm

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

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

1487 where

1504 where

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

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

1489 ai qq env ds (PRef fc f)

1506 ai qq env ds (PRef fc f)

1490 | f `elem` infns = PInferRef fc f

1507 | f `elem` infns = PInferRef fc f

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

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

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

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

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

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

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

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

1495 = let lt' = ai qq env ds lt

1512 = let lt' = ai qq env ds lt

1496 rt' = ai qq env ds rt

1513 rt' = ai qq env ds rt

@@ -1526,7 +1543,7 @@ addImpl' inpat env infns ist ptm

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

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

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

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

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

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

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

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

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

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

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

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

1532 arity = getPArity ty in

1549 arity = getPArity ty in

@@ -1561,7 +1578,9 @@ addImpl' inpat env infns ist ptm

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

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

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

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

1563 = let ty' = ai qq env ds ty

1580 = let ty' = ai qq env ds ty

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

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

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

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

1565 PPi p n ty' sc'

1584 PPi p n ty' sc'

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

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

1567 = let r' = ai qq env ds r

1586 = let r' = ai qq env ds r

@@ -1585,8 +1604,8 @@ addImpl' inpat env infns ist ptm

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

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

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

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

1587

1606

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

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

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

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

1590 = case lookupDef f (tt_ctxt ist) of

1609 = case lookupDef f (tt_ctxt ist) of

1591 [] -> Right $ PPatvar fc f

1610 [] -> Right $ PPatvar fc f

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

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

@@ -1594,7 +1613,7 @@ aiFn inpat True qq ist fc f ds []

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

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

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

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

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

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

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

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

1598 else Right $ PPatvar fc f

1617 else Right $ PPatvar fc f

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

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

1600 imp _ = True

1619 imp _ = True

@@ -1608,9 +1627,9 @@ aiFn inpat True qq ist fc f ds []

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

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

1609 vname _ = False

1628 vname _ = False

1610

1629

1611−aiFn inpat expat qq ist fc f ds as

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

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

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

1613−aiFn inpat expat qq ist fc f ds as

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

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

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

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

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

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

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

@@ -1618,15 +1637,20 @@ aiFn inpat expat qq ist fc f ds as

1618 [] -> nh

1637 [] -> nh

1619 x -> x

1638 x -> x

1620 case ns' of

1639 case ns' of

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

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

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

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

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

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

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

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

1625 alts -> Right $

1644 alts -> Right $

1626 PAlternative True $

1645 PAlternative True $

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

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

1628 (insertImpl ns as)) alts

1647 (insertImpl ns as)) alts

1629 where

1648 where

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

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

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

1652+ | otherwise = f'

1653+

1630 trimAlts [] alts = alts

1654 trimAlts [] alts = alts

1631 trimAlts ns alts

1655 trimAlts ns alts

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

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

@@ -1670,7 +1694,7 @@ aiFn inpat expat qq ist fc f ds as

1670 PImp p True l n Placeholder :

1694 PImp p True l n Placeholder :

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

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

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

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

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

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

1674 case find n imps [] of

1698 case find n imps [] of

1675 Just (tm, imps') ->

1699 Just (tm, imps') ->

1676 PTacImplicit p l n sc tm :

1700 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+25−15

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

@@ -594,20 +598,20 @@ data PDecl' t

594 | PNamespace String [PDecl' t] -- ^ New namespace

598 | PNamespace String [PDecl' t] -- ^ New namespace

595 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts

599 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts

596 Name -- Record name

600 Name -- Record name

597− [(Name, Plicity, t)] -- Params

601+ [(Name, Plicity, t)] -- Parameters

598− [(Name, Docstring (Either Err PTerm))] -- Params doc

602+ [(Name, Docstring (Either Err PTerm))] -- Parameter docs

599 [(Name, Plicity, t)] -- Fields

603 [(Name, Plicity, t)] -- Fields

600 [(Name, Docstring (Either Err PTerm))] -- Fields doc

604 [(Name, Docstring (Either Err PTerm))] -- Fields doc

601 (Maybe Name) -- Optional constructor name

605 (Maybe Name) -- Optional constructor name

602 (Docstring (Either Err PTerm)) -- Constructor doc

606 (Docstring (Either Err PTerm)) -- Constructor doc

603 SyntaxInfo -- Constructor SyntaxInfo

607 SyntaxInfo -- Constructor SyntaxInfo

604 -- ^ Record declaration

608 -- ^ Record declaration

605− -- (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) (Maybe Name) t -- ^ Record declaration

606 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

609 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

607 [(Name, t)] -- constraints

610 [(Name, t)] -- constraints

608 Name

611 Name

609 [(Name, t)] -- parameters

612 [(Name, t)] -- parameters

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

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

614+ [Name] -- determining parameters

611 [PDecl' t] -- declarations

615 [PDecl' t] -- declarations

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

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

613 -- class name, parameters, method declarations

617 -- class name, parameters, method declarations

@@ -640,10 +644,12 @@ deriving instance NFData PDecl'

640-- For elaborator state

644-- For elaborator state

641data EState = EState {

645data EState = EState {

642 case_decls :: [PDecl],

646 case_decls :: [PDecl],

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

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

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

644 }

649 }

645

650

646−initEState = EState [] []

651+initEState :: EState

652+initEState = EState [] [] []

647

653

648type ElabD a = Elab' EState a

654type ElabD a = Elab' EState a

649

655

@@ -701,9 +707,9 @@ declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

701declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

707declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

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

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

703declared (PNamespace _ ds) = concatMap declared ds

709declared (PNamespace _ ds) = concatMap declared ds

704−declared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn

710+declared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : maybeToList cn -- : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn

705 where fstt (a, _, _) = a

711 where fstt (a, _, _) = a

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

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

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

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

708declared (PDSL n _) = [n]

714declared (PDSL n _) = [n]

709declared (PSyntax _ _) = []

715declared (PSyntax _ _) = []

@@ -717,14 +723,14 @@ tldeclared (PFix _ _ _) = []

717tldeclared (PTy _ _ _ _ _ n t) = [n]

723tldeclared (PTy _ _ _ _ _ n t) = [n]

718tldeclared (PPostulate _ _ _ _ n t) = [n]

724tldeclared (PPostulate _ _ _ _ n t) = [n]

719tldeclared (PClauses _ _ n _) = [] -- not a declaration

725tldeclared (PClauses _ _ n _) = [] -- not a declaration

720−tldeclared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn

726+tldeclared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : maybeToList cn -- (map fstt ps) ++ (map fstt fs) ++ maybeToList cn

721 where fstt (a, _, _) = a

727 where fstt (a, _, _) = a

722tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

728tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

723 where fstt (_, _, a, _, _, _) = a

729 where fstt (_, _, a, _, _, _) = a

724tldeclared (PParams _ _ ds) = []

730tldeclared (PParams _ _ ds) = []

725tldeclared (PMutual _ ds) = concatMap tldeclared ds

731tldeclared (PMutual _ ds) = concatMap tldeclared ds

726tldeclared (PNamespace _ ds) = concatMap tldeclared ds

732tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

729tldeclared _ = []

735tldeclared _ = []

730

736

@@ -739,9 +745,9 @@ defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

739defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

745defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

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

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

741defined (PNamespace _ ds) = concatMap defined ds

747defined (PNamespace _ ds) = concatMap defined ds

742−defined (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn

748+defined (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : maybeToList cn -- (map fstt ps) ++ (map fstt fs) ++ maybeToList cn

743 where fstt (a, _, _) = a

749 where fstt (a, _, _) = a

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

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

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

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

746defined (PDSL n _) = [n]

752defined (PDSL n _) = [n]

747defined (PSyntax _ _) = []

753defined (PSyntax _ _) = []

@@ -1042,7 +1048,8 @@ data ClassInfo = CI { instanceName :: Name,

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

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

1043 class_default_superclasses :: [PDecl],

1049 class_default_superclasses :: [PDecl],

1044 class_params :: [Name],

1050 class_params :: [Name],

1045− class_instances :: [Name] }

1051+ class_instances :: [Name],

1052+ class_determiners :: [Int] }

1046 deriving Show

1053 deriving Show

1047{-!

1054{-!

1048deriving instance Binary ClassInfo

1055deriving instance Binary ClassInfo

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

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

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

1204 syn_namespace :: [String],

1211 syn_namespace :: [String],

1205 no_imp :: [Name],

1212 no_imp :: [Name],

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

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

1215+ -- binders

1206 decoration :: Name -> Name,

1216 decoration :: Name -> Name,

1207 inPattern :: Bool,

1217 inPattern :: Bool,

1208 implicitAllowed :: Bool,

1218 implicitAllowed :: Bool,

@@ -1216,7 +1226,7 @@ deriving instance NFData SyntaxInfo

1216deriving instance Binary SyntaxInfo

1226deriving instance Binary SyntaxInfo

1217!-}

1227!-}

1218

1228

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

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

1220

1230

1221expandNS :: SyntaxInfo -> Name -> Name

1231expandNS :: SyntaxInfo -> Name -> Name

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Core/Binary.hs+15−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,12 @@ 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

152+ put (InvalidTCArg n t) = do putWord8 38

153+ put n

154+ put t

149

155

150 get = do i <- getWord8

156 get = do i <- getWord8

151 case i of

157 case i of

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

172 13 -> fmap NoTypeDecl get

178 13 -> fmap NoTypeDecl get

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

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

174 return $ NotInjective x y z

180 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

181+ 15 -> fmap (CantResolve False) get

176 16 -> fmap CantResolveAlts get

182 16 -> fmap CantResolveAlts get

177 17 -> fmap IncompleteTerm get

183 17 -> fmap IncompleteTerm get

178 18 -> return UniverseError

184 18 -> return UniverseError

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

205 x2 <- get

211 x2 <- get

206 x3 <- get

212 x3 <- get

207 return (ElabDebug x1 x2 x3)

213 return (ElabDebug x1 x2 x3)

214+ 37 -> do x1 <- get

215+ x2 <- get

216+ return (NoEliminator x1 x2)

217+ 38 -> do x1 <- get

218+ x2 <- get

219+ return (InvalidTCArg x1 x2)

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

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

209----- Generated by 'derive'

221----- Generated by 'derive'

210

222

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

@@ -80,9 +80,11 @@ 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 (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

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

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

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

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

86 rnf UniverseError = ()

88 rnf UniverseError = ()

87 rnf ProgramLineComment = ()

89 rnf ProgramLineComment = ()

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

90 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+38−14

@@ -155,9 +155,12 @@ 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

160+ | InvalidTCArg Name t

159 | CantResolveAlts [Name]

161 | CantResolveAlts [Name]

160 | IncompleteTerm t

162 | IncompleteTerm t

163+ | NoEliminator String t

161 | UniverseError

164 | UniverseError

162 | UniqueError Universe Name

165 | UniqueError Universe Name

163 | UniqueKindError Universe Name

166 | UniqueKindError Universe Name

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

231 size (NoSuchVariable name) = size name

234 size (NoSuchVariable name) = size name

232 size (NoTypeDecl name) = size name

235 size (NoTypeDecl name) = size name

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

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

234− size (CantResolve trm) = size trm

237+ size (CantResolve _ trm) = size trm

235 size (NoRewriting trm) = size trm

238 size (NoRewriting trm) = size trm

236 size (CantResolveAlts _) = 1

239 size (CantResolveAlts _) = 1

237 size (IncompleteTerm trm) = size trm

240 size (IncompleteTerm trm) = size trm

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

246

249

247score :: Err -> Int

250score :: Err -> Int

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

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

249−score (CantResolve _) = 20

252+score (CantResolve _ _) = 20

250score (NoSuchVariable _) = 1000

253score (NoSuchVariable _) = 1000

251score (ProofSearchFail e) = score e

254score (ProofSearchFail e) = score e

252score (CantSolveGoal _ _) = 100000

255score (CantSolveGoal _ _) = 100000

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

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

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

508 concatMap (Map.toList) allns

511 concatMap (Map.toList) allns

509

512

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

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

511addAlist [] ctxt = ctxt

514addAlist [] ctxt = ctxt

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

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

513

516

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

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

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

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

938instantiate :: TT n -> TT n -> TT n

936instantiate e = subst 0 where

939instantiate e = subst 0 where

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

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

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

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

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

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

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

945-- that has been substituted.

949-- that has been substituted.

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

950substV :: TT n -> TT n -> TT n

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

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

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

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

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

949 | otherwise = V x

954 | otherwise = V x

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

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

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

1038 -- substitution happens...)

1043 -- substitution happens...)

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1163,17 +1171,33 @@ unList tm = case unApply tm of

1163forget :: TT Name -> Raw

1171forget :: TT Name -> Raw

1164forget tm = forgetEnv [] tm

1172forget tm = forgetEnv [] tm

1165

1173

1174+safeForget :: TT Name -> Maybe Raw

1175+safeForget tm = safeForgetEnv [] tm

1176+

1166forgetEnv :: [Name] -> TT Name -> Raw

1177forgetEnv :: [Name] -> TT Name -> Raw

1167−forgetEnv env (P _ n _) = Var n

1178+forgetEnv env tm = case safeForgetEnv env tm of

1179+ Just t' -> t'

1180+ Nothing -> error $ "Scope error in " ++ show tm

1181+

1182+

1183+safeForgetEnv :: [Name] -> TT Name -> Maybe Raw

1184+safeForgetEnv env (P _ n _) = Just $ Var n

1168−forgetEnv env (V i) = Var (env !! i)

1185+safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)

1186+ | otherwise = Nothing

1187+safeForgetEnv env (Bind n b sc)

1169−forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1188+ = do let n' = uniqueName n env

1170− RBind n' (fmap (forgetEnv env) b)

1189+ b' <- safeForgetEnvB env b

1171− (forgetEnv (n':env) sc)

1190+ sc' <- safeForgetEnv (n':env) sc

1172−forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)

1191+ Just $ RBind n' b' sc'

1192+ where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)

1193+ (safeForgetEnv env v)

1194+ safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

1195+ Just $ fmap (\_ -> ty') b

1196+safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

1173−forgetEnv env (Constant c) = RConstant c

1197+safeForgetEnv env (Constant c) = Just $ RConstant c

1174−forgetEnv env (TType i) = RType

1198+safeForgetEnv env (TType i) = Just RType

1175−forgetEnv env (UType u) = RUType u

1199+safeForgetEnv env (UType u) = Just $ RUType u

1176−forgetEnv env Erased = RConstant Forgot

1200+safeForgetEnv env Erased = Just $ RConstant Forgot

1177

1201

1178-- | Introduce a 'Bind' into the given term for each element of the

1202-- | Introduce a 'Bind' into the given term for each element of the

1179-- given list of (name, binder) pairs.

1203-- given list of (name, binder) pairs.

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` rnf x10 `seq` rnf x11 `seq` rnf x12 `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+11−1

@@ -289,7 +289,11 @@ 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)

293+pprintErr' i (InvalidTCArg n t)

294+ = annTm t (pprintTerm i (delab i t)) <+> text " cannot be a parameter of "

295+ <> annName n <$>

296+ text "(Type class arguments must be injective)"

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

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

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

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

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

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

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

299pprintErr' i (CantMatch t) =

303pprintErr' i (CantMatch t) =

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

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

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

306+pprintErr' i (NoEliminator s t)

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

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

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

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

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

302pprintErr' i UniverseError = text "Universe inconsistency"

312pprintErr' i UniverseError = text "Universe inconsistency"

303pprintErr' i (UniqueError NullType n)

313pprintErr' i (UniqueError NullType n)

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

314 = 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+44−32

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

@@ -600,7 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

600 -- If we're inferring metavariables in the type, don't recheck,

603 -- If we're inferring metavariables in the type, don't recheck,

601 -- because we're only doing this to try to work out those metavariables

604 -- because we're only doing this to try to work out those metavariables

602 (clhs_c, clhsty) <- if not inf

605 (clhs_c, clhsty) <- if not inf

603− then recheckC fc [] lhs_tm

606+ then recheckC fc id [] lhs_tm

604 else return (lhs_tm, lhs_ty)

607 else return (lhs_tm, lhs_ty)

605 let clhs = normalise ctxt [] clhs_c

608 let clhs = normalise ctxt [] clhs_c

606 let borrowed = borrowedNames [] clhs

609 let borrowed = borrowedNames [] clhs

@@ -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,15 +672,16 @@ 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"

676 logLvl 4 $ "---> " ++ show rhs'

681 logLvl 4 $ "---> " ++ show rhs'

677 when (not (null defer)) $ iLOG $ "DEFERRED " ++

682 when (not (null defer)) $ iLOG $ "DEFERRED " ++

678 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

683 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

679− def' <- checkDef fc defer

684+ def' <- checkDef fc (Elaborating "deferred type of ") defer

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

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

681 addDeferred def''

686 addDeferred def''

682 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

687 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

@@ -695,7 +700,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

695 logLvl 6 $ " ==> " ++ show (forget rhs')

700 logLvl 6 $ " ==> " ++ show (forget rhs')

696

701

697 (crhs, crhsty) <- if not inf

702 (crhs, crhsty) <- if not inf

698− then recheckC_borrowing True borrowed fc [] rhs'

703+ then recheckC_borrowing True borrowed fc id [] rhs'

699 else return (rhs', clhsty)

704 else return (rhs', clhsty)

700 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

705 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

701 ctxt <- getContext

706 ctxt <- getContext

@@ -812,38 +817,42 @@ 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))

822 let static_names = getStaticNames i lhs_tm

829 let static_names = getStaticNames i lhs_tm

823 logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)

830 logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)

824− (clhs, clhsty) <- recheckC fc [] lhs_tm

831+ (clhs, clhsty) <- recheckC fc id [] lhs_tm

825 logLvl 5 ("Checked " ++ show clhs)

832 logLvl 5 ("Checked " ++ show clhs)

826 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

833 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

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

844 mapM_ (elabCaseBlock info opts) is

853 mapM_ (elabCaseBlock info opts) is

845 logLvl 5 ("Checked wval " ++ show wval')

854 logLvl 5 ("Checked wval " ++ show wval')

846− (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

855+ (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')

847 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

856 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

848 let cwvalN = explicitNames (normalise ctxt [] cwval)

857 let cwvalN = explicitNames (normalise ctxt [] cwval)

849 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

858 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

@@ -898,7 +907,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

898 addIBC (IBCImp wname)

907 addIBC (IBCImp wname)

899 addIBC (IBCStatic wname)

908 addIBC (IBCStatic wname)

900

909

901− def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

910+ def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]

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

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

903 addDeferred def''

912 addDeferred def''

904

913

@@ -923,20 +932,23 @@ 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 iderr 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''

937 mapM_ (elabCaseBlock info opts) is

949 mapM_ (elabCaseBlock info opts) is

938 logLvl 5 ("Checked RHS " ++ show rhs')

950 logLvl 5 ("Checked RHS " ++ show rhs')

939− (crhs, crhsty) <- recheckC fc [] rhs'

951+ (crhs, crhsty) <- recheckC fc id [] rhs'

940 return $ (Right (clhs, crhs), lhs)

952 return $ (Right (clhs, crhs), lhs)

941 where

953 where

942 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

954 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

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+52−13

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

@@ -135,6 +135,8 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

135 [PClause fc iname lhs [] rhs wb]]

136 iLOG (show idecls)

137 mapM_ (rec_elabDecl info EAll info) idecls

138+ ist <- getIState

139+ checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

138 addIBC (IBCInstance intInst n iname)

140 addIBC (IBCInstance intInst n iname)

139

141

140 where

142 where

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

167 = do ty' <- addUsingConstraints syn fc t

169 = do ty' <- addUsingConstraints syn fc t

168 -- TODO think: something more in info?

170 -- TODO think: something more in info?

169 ty' <- implicit info syn iname ty'

171 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

172+ let ty = addImpl [] i ty'

171 ctxt <- getContext

173 ctxt <- getContext

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

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

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

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

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

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

177+ setContext ctxt'

178+ processTacticDecls newDecls

175 ctxt <- getContext

179 ctxt <- getContext

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

180+ (cty, _) <- recheckC fc id [] tyT

177 let nty = normalise ctxt [] cty

181 let nty = normalise ctxt [] cty

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

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

179

183

180− findOverlapping i t n

184+ findOverlapping i dets t n

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

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

182 | otherwise

186 | otherwise

183 = case lookupTy n (tt_ctxt i) of

187 = case lookupTy n (tt_ctxt i) of

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

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

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

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

186− case matchClause i tret' tret of

190+ case matchArgs i dets tret' tret of

187− Right ms -> Just tret'

191+ Right _ -> Just tret'

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

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

189− Right ms -> Just tret'

193+ Right _ -> Just tret'

190− Left _ -> Nothing

194+ Left _ -> Nothing

191 _ -> Nothing

195 _ -> Nothing

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

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

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

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

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

198 getRetType (PPi _ _ _ sc) = getRetType sc

195 getRetType t = t

199 getRetType t = t

196

200

201+ matchArgs i dets x y =

202+ let x' = keepDets dets x

203+ y' = keepDets dets y in

204+ matchClause i x' y'

205+

206+ keepDets dets (PApp fc f args)

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

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

209+ keepDets dets t = t

210+

197 mkMethApp (n, _, _, ty)

211 mkMethApp (n, _, _, ty)

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

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

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

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

@@ -264,3 +278,28 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

264 clauseFor m iname ns (PClauses _ _ m' _)

278 clauseFor m iname ns (PClauses _ _ m' _)

265 = decorate ns iname m == decorate ns iname m'

279 = decorate ns iname m == decorate ns iname m'

266 clauseFor m iname ns _ = False

280 clauseFor m iname ns _ = False

281+

282+checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

283+checkInjectiveArgs fc n ds Nothing = return ()

284+checkInjectiveArgs fc n ds (Just ty)

285+ = do ist <- getIState

286+ let (_, args) = unApply (instantiateRetTy ty)

287+ ci 0 ist args

288+ where

289+ ci i ist (a : as) | i `elem` ds

290+ = if isInj ist a then ci (i + 1) ist as

291+ else tclift $ tfail (At fc (InvalidTCArg n a))

292+ ci i ist (a : as) = ci (i + 1) ist as

293+ ci i ist [] = return ()

294+

295+ isInj i (P Bound n _) = True

296+ isInj i (P _ n _) = isConName n (tt_ctxt i)

297+ isInj i (App f a) = isInj i f && isInj i a

298+ isInj i (V _) = True

299+ isInj i (Bind n b sc) = isInj i sc

300+ isInj _ _ = True

301+

302+ instantiateRetTy (Bind n (Pi _ _ _) sc)

303+ = substV (P Bound n Erased) (instantiateRetTy sc)

304+ instantiateRetTy t = t

305+

src/Idris/Elab/Record.hs+73−63

@@ -30,51 +30,54 @@ elabRecord :: ElabInfo ->

30 SyntaxInfo -> -- ^ Constructor SyntaxInfo

31 Idris ()

32elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdoc csyn

33− = do logLvl 2 $ "Building data declaration for " ++ show tyn

33+ = do logLvl 1 $ "Building data declaration for " ++ show tyn

34 -- Type constructor

35− let tycon = generateTyCon params

35+ let tycon = generateTyConType params

36− logLvl 4 $ "Type constructor " ++ showTmImpls tycon

36+ logLvl 1 $ "Type constructor " ++ showTmImpls tycon

37

38 -- Data constructor

39 dconName <- generateDConName cname

40− let dcon = generateDCon params fields

40+ let dconTy = generateDConType params fields

41− logLvl 4 $ "Data constructor: " ++ showTmImpls dcon

41+ logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

42

43 -- Build data declaration for elaboration

44− let datadecl = PDatadecl tyn tycon [(cdoc, [], dconName, dcon, fc, [])]

44+ let datadecl = PDatadecl tyn tycon [(cdoc, [], dconName, dconTy, fc, [])]

45 elabData info rsyn doc [] fc opts datadecl

46

47 i <- getIState

48

49− -- The elaborated constructor for the data declaration

49+ -- The elaborated constructor type for the data declaration

50− ttCons <-

50+ ttConsTy <-

51 case lookupTyExact dconName (tt_ctxt i) of

52 Just as -> return as

53− Nothing -> tclift $ tfail $ At fc (Elaborating "record" tyn (Msg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

53+ Nothing -> tclift $ tfail $ At fc (Elaborating "record" tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

54

55 -- The arguments to the constructor

56− let constructorArgs = getArgTys ttCons

56+ let constructorArgs = getArgTys ttConsTy

57 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.

58 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)

59

60 -- The parameters for elaboration with their documentation

61+ -- Parameter functions are all prefixed with "param_".

61− let paramsForElab = [((nsroot n), (param_name n), impl, t, d) | (n, t, d) <- zip' i params paramDocs]

62+ let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, t, d) <- zipParams i params paramDocs]

62

63

63 -- The fields (written by the user) with their documentation.

64 -- The fields (written by the user) with their documentation.

64 let userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]

65 let userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]

65

66

66 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

67 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

67− let fieldsForElab = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

68+ let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

68−

69− -- Build projection functions

69+ -- Build and elaborate projection functions

70− elabProj dconName fieldsForElab

70+ elabProj dconName projectors

71+

72+ -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.

73+ let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]

71− -- Build update functions

74+ -- Build and elaborate update functions

72− elabUp dconName [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]

75+ elabUp dconName updaters

73 where

76 where

74 -- | Generates a type constructor.

77 -- | Generates a type constructor.

75− generateTyCon :: [(Name, Plicity, PTerm)] -> PTerm

78+ generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm

76− generateTyCon ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyCon rest)

79+ generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)

77− generateTyCon [] = PType

80+ generateTyConType [] = PType

78

81

79 -- | Generates a name for the data constructor if none was specified.

82 -- | Generates a name for the data constructor if none was specified.

80 generateDConName :: Maybe Name -> Idris Name

83 generateDConName :: Maybe Name -> Idris Name

@@ -88,18 +91,18 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

88 Nothing -> return n

91 Nothing -> return n

89

92

90 -- | Generates the data constructor type.

93 -- | Generates the data constructor type.

91− generateDCon :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

94+ generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

92− generateDCon ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDCon ps as)

95+ generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)

93− generateDCon [] ((n, p, t) : as) = PPi p (nsroot n) t (generateDCon [] as)

96+ generateDConType [] ((n, p, t) : as) = PPi p (nsroot n) t (generateDConType [] as)

94− generateDCon [] [] = target

97+ generateDConType [] [] = target

95

98

96 -- | Creates an PArg from a plicity and a name where the term is a PRef.

99 -- | Creates an PArg from a plicity and a name where the term is a PRef.

97− paramAsArg :: Plicity -> Name -> PArg

100+ asPRefArg :: Plicity -> Name -> PArg

98− paramAsArg p n = asArg p (nsroot n) $ PRef fc (nsroot n)

101+ asPRefArg p n = asArg p (nsroot n) $ PRef fc (nsroot n)

99

102

100 -- | The target for the constructor and projection functions. Also the source of the update functions.

103 -- | The target for the constructor and projection functions. Also the source of the update functions.

101 target :: PTerm

104 target :: PTerm

102− target = PApp fc (PRef fc tyn) $ map (uncurry paramAsArg) [(p, n) | (n, p, t) <- params]

105+ target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, t) <- params]

103

106

104 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.

107 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.

105 placeholderArg :: Plicity -> Name -> PArg

108 placeholderArg :: Plicity -> Name -> PArg

@@ -127,50 +130,57 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

127 fieldTerms :: [PTerm]

130 fieldTerms :: [PTerm]

128 fieldTerms = [t | (_, _, t) <- fields]

131 fieldTerms = [t | (_, _, t) <- fields]

129

132

130− projectInType :: [(Name, Name)] -> PTerm -> PTerm

131− projectInType xs = mapPT st

132− where

133− st :: PTerm -> PTerm

134− st (PRef fc n)

135− | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]

136− st t = t

137−

138 -- Delabs the TT to PTerm

133 -- Delabs the TT to PTerm

139 -- This is not good.

134 -- This is not good.

140 -- However, for machine generated implicits, there seems to be no PTerm available.

135 -- However, for machine generated implicits, there seems to be no PTerm available.

141 -- Is there a better way to do this without building the setters and getters as TT?

136 -- Is there a better way to do this without building the setters and getters as TT?

142 freeField :: IState -> (Name, TT Name) -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))

137 freeField :: IState -> (Name, TT Name) -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))

143− freeField i arg = (fst arg, (expandNS rsyn (free_name $ fst arg)), impl, (delab i (snd arg)), emptyDocstring)

138+ freeField i arg = let nameInCons = fst arg -- The name as it appears in the constructor

144−

139+ nameFree = expandNS rsyn (freeName $ fst arg) -- The name prefixed with "free_"

140+ plicity = impl -- All free fields are implicit as they are machine generated

141+ fieldType = delab i (snd arg) -- The type of the field

142+ doc = emptyDocstring -- No docmentation for machine generated fields

143+ in (nameInCons, nameFree, plicity, fieldType, doc)

144+

145− free_name :: Name -> Name

145+ freeName :: Name -> Name

146− free_name (UN n) = sUN ("free_" ++ str n)

146+ freeName (UN n) = sUN ("free_" ++ str n)

147− free_name (MN i n) = sMN i ("free_" ++ str n)

147+ freeName (MN i n) = sMN i ("free_" ++ str n)

148− free_name (NS n s) = NS (free_name n) s

148+ freeName (NS n s) = NS (freeName n) s

149− free_name n = n

149+ freeName n = n

150−

150+

151+ -- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.

151− zip' :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]

152+ zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]

152− zip' i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zip' i rest rest')

153+ zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')

153− zip' i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zip' i rest [])

154+ zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])

154 where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring

155 where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring

155− zip' _ [] [] = []

156+ zipParams _ [] [] = []

156

157

157− param_name :: Name -> Name

158+ paramName :: Name -> Name

158− param_name (UN n) = sUN ("param_" ++ str n)

159+ paramName (UN n) = sUN ("param_" ++ str n)

159− param_name (MN i n) = sMN i ("param_" ++ str n)

160+ paramName (MN i n) = sMN i ("param_" ++ str n)

160− param_name (NS n s) = NS (param_name n) s

161+ paramName (NS n s) = NS (paramName n) s

161− param_name n = n

162+ paramName n = n

162

163

163 -- | Elaborate the projection functions.

164 -- | Elaborate the projection functions.

164 elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

165 elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

165 elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

166 elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

166 elab = \(n, n', p, t, doc, i) ->

167 elab = \(n, n', p, t, doc, i) ->

168+ -- Use projections in types

167 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs] t

169 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs] t

168 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i

170 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i

169 in mapM_ elab fs

171 in mapM_ elab fs

170

172

173+ projectInType :: [(Name, Name)] -> PTerm -> PTerm

174+ projectInType xs = mapPT st

175+ where

176+ st :: PTerm -> PTerm

177+ st (PRef fc n)

178+ | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]

179+ st t = t

180+

171 -- | Elaborate the update functions.

181 -- | Elaborate the update functions.

172 elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

182 elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

173− elabUp cn fs = let args = map (uncurry paramAsArg) [(p, n) | (n, _, p, _, _, _) <- fs]

183+ elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

174 elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

184 elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

175 in mapM_ elab fs

185 in mapM_ elab fs

176

186

@@ -180,7 +190,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

180

190

181 -- | A map from a field name to the other fields it depends on.

191 -- | A map from a field name to the other fields it depends on.

182 fieldDependencies :: [(Name, [Name])]

192 fieldDependencies :: [(Name, [Name])]

183− fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields]

193+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]

184 where

194 where

185 fieldDep :: Name -> PTerm -> (Name, [Name])

195 fieldDep :: Name -> PTerm -> (Name, [Name])

186 fieldDep n t = ((nsroot n), fieldNames `intersect` allNamesIn t)

196 fieldDep n t = ((nsroot n), fieldNames `intersect` allNamesIn t)

@@ -214,15 +224,15 @@ elabProjection :: ElabInfo ->

214 Int -> -- ^ Argument Index

224 Int -> -- ^ Argument Index

215 Idris ()

225 Idris ()

216elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames index

226elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames index

217− = do logLvl 2 $ "Generating Projection for " ++ show pname

227+ = do logLvl 1 $ "Generating Projection for " ++ show pname

218

228

219 let ty = generateTy

229 let ty = generateTy

220− logLvl 4 $ "Type of " ++ show pname ++ ": " ++ show ty

230+ logLvl 1 $ "Type of " ++ show pname ++ ": " ++ show ty

221

231

222 let lhs = generateLhs

232 let lhs = generateLhs

223− logLvl 4 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

233+ logLvl 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

224 let rhs = generateRhs

234 let rhs = generateRhs

225− logLvl 4 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

235+ logLvl 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

226

236

227 rec_elabDecl info EAll info ty

237 rec_elabDecl info EAll info ty

228

238

@@ -278,23 +288,23 @@ elabUpdate :: ElabInfo ->

278 Bool -> -- ^ Optional

288 Bool -> -- ^ Optional

279 Idris ()

289 Idris ()

280elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

290elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

281− = do logLvl 2 $ "Generating Update for " ++ show pname

291+ = do logLvl 1 $ "Generating Update for " ++ show pname

282

292

283 let ty = generateTy

293 let ty = generateTy

284− logLvl 4 $ "Type of " ++ show set_pname ++ ": " ++ show ty

294+ logLvl 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty

285

295

286 let lhs = generateLhs

296 let lhs = generateLhs

287− logLvl 4 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

297+ logLvl 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

288

298

289 let rhs = generateRhs

299 let rhs = generateRhs

290− logLvl 4 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

300+ logLvl 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

291

301

292 let clause = PClause fc set_pname lhs [] rhs []

302 let clause = PClause fc set_pname lhs [] rhs []

293

303

294 idrisCatch (do rec_elabDecl info EAll info ty

304 idrisCatch (do rec_elabDecl info EAll info ty

295 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])

305 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])

296 (\err -> if optional

306 (\err -> if optional

297− then logLvl 2 $ "Could not generate update function for " ++ show pname

307+ then logLvl 1 $ "Could not generate update function for " ++ show pname

298 else tclift $ tfail $ At fc (Elaborating "record update function" pname err))

308 else tclift $ tfail $ At fc (Elaborating "record update function" pname err))

299 where

309 where

300 -- | The type of the udpate function.

310 -- | The type of the udpate function.

src/Idris/Elab/Transform.hs+12−6

@@ -53,28 +53,34 @@ 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

63

65

64− (clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm

66+ (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

65 let clhs_tm = renamepats pnames clhs_tm_in

67 let clhs_tm = renamepats pnames clhs_tm_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 id [] 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)

80

86

src/Idris/Elab/Type.hs+17−13

@@ -57,23 +57,25 @@ 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

74 logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

76 logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

75

77

76− ds <- checkAddDef True False fc defer

78+ ds <- checkAddDef True False fc iderr defer

77 -- if the type is not complete, note that we'll need to infer

79 -- if the type is not complete, note that we'll need to infer

78 -- things later (for solving metavariables)

80 -- things later (for solving metavariables)

79 when (not (null ds)) $ addTyInferred n

81 when (not (null ds)) $ addTyInferred n

@@ -83,7 +85,7 @@ buildType info syn fc opts n ty' = do

83 logLvl 5 $ "Rechecking"

85 logLvl 5 $ "Rechecking"

84 logLvl 6 $ show tyT

86 logLvl 6 $ show tyT

85 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

87 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

86− (cty, ckind) <- recheckC fc [] tyT

88+ (cty, ckind) <- recheckC fc id [] tyT

87

89

88 -- record the implicit and inaccessible arguments

90 -- record the implicit and inaccessible arguments

89 i <- getIState

91 i <- getIState

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

@@ -150,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

150 -- Productivity checking now via checking for guarded 'Delay'

154 -- Productivity checking now via checking for guarded 'Delay'

151 let opts' = opts -- if corec then (Coinductive : opts) else opts

155 let opts' = opts -- if corec then (Coinductive : opts) else opts

152 let usety = if norm then nty' else nty

156 let usety = if norm then nty' else nty

153− ds <- checkDef fc [(n, (-1, Nothing, usety))]

157+ ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

154 addIBC (IBCDef n)

158 addIBC (IBCDef n)

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

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

156 addDeferred ds'

160 addDeferred ds'

src/Idris/Elab/Utils.hs+23−15

@@ -22,31 +22,41 @@ import Debug.Trace

22

23import qualified Data.Map as Map

24

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

26

27−recheckC_borrowing uniq_check bs fc env t

27+recheckC_borrowing uniq_check bs fc mkerr env t

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

29 ctxt <- getContext

30+ t' <- case safeForget t of

31+ Just ft -> return ft

32+ Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

30− (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of

33+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

31− Error e -> tfail (At fc e)

34+ Error e -> tfail (At fc (mkerr e))

32 OK x -> return x

35 OK x -> return x

33 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

36 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

34 addConstraints fc cs

37 addConstraints fc cs

35 return (tm, ty)

38 return (tm, ty)

36

39

40+iderr :: Name -> Err -> Err

41+iderr _ e = e

37

42

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

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

38−checkDef fc ns = checkAddDef False True fc ns

45+checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

39

46

47+checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

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

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

40−checkAddDef add toplvl fc [] = return []

50+checkAddDef add toplvl fc mkerr [] = return []

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

51+checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)

42 = do ctxt <- getContext

52 = do ctxt <- getContext

43− (t', _) <- recheckC fc [] t

53+ (t', _) <- recheckC fc (mkerr n) [] t

44 when add $ do addDeferred [(n, (i, top, t, toplvl))]

54 when add $ do addDeferred [(n, (i, top, t, toplvl))]

45 addIBC (IBCDef n)

55 addIBC (IBCDef n)

46− ns' <- checkAddDef add toplvl fc ns

56+ ns' <- checkAddDef add toplvl fc mkerr ns

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

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

48

58

49−-- Get the list of (index, name) of inaccessible arguments from an elaborated

59+-- | Get the list of (index, name) of inaccessible arguments from an elaborated

50-- type

60-- type

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

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

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

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

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

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

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

55inaccessibleImps _ _ _ = []

65inaccessibleImps _ _ _ = []

56

66

57−-- Get the list of (index, name) of inaccessible arguments from the type.

67+-- | Get the list of (index, name) of inaccessible arguments from the type.

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

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

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

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

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

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

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

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

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

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

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

76

86

77−-- Check that the result of type checking matches what the programmer wrote

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

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

79-- they are the same!)

89-- they are the same!)

80−

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

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

82checkInferred fc inf user =

91checkInferred fc inf user =

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

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

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

92 logLvl 10 $ "Checked match"

101 logLvl 10 $ "Checked match"

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

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

94

103

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

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

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

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

97−

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

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

99inferredDiff fc inf user =

107inferredDiff fc inf user =

100 do i <- getIState

108 do i <- getIState

src/Idris/Elab/Value.hs+11−6

@@ -56,25 +56,30 @@ 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)") iderr defer

72 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

77 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

73 addDeferred def''

78 addDeferred def''

74 mapM_ (elabCaseBlock info []) is

79 mapM_ (elabCaseBlock info []) is

75

80

76 logLvl 3 ("Value: " ++ show vtm)

81 logLvl 3 ("Value: " ++ show vtm)

77− (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm

82+ (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

78

83

79 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

84 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

80 else vtm_in

85 else vtm_in

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+214−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 iderr [(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,9 +1375,12 @@ 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 _] -> filter accessible ins

1350 _ -> []

1379 _ -> []

1351 | otherwise = []

1380 | otherwise = []

1381+ where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

1382+ Just (_, Hidden) -> False

1383+ _ -> True

1352

1384

1353-- Try again to solve auto implicits

1385-- Try again to solve auto implicits

1354solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

1386solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

@@ -1376,14 +1408,26 @@ proofSearch' ist rec ambigok depth prv top n hints

1376-- Resolve type classes. This will only pick up 'normal' instances, never

1408-- Resolve type classes. This will only pick up 'normal' instances, never

1377-- named instances (hence using 'tcname' to check it's a generated instance

1409-- named instances (hence using 'tcname' to check it's a generated instance

1378-- name).

1410-- name).

1411+resolveTC :: Bool -- using default Int

1412+ -> Bool -- allow metavariables in the goal

1413+ -> Int -- depth

1414+ -> Term -- top level goal

1415+ -> Name -- top level function name

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1416+ -> IState -> ElabD ()

1380−resolveTC = resTC' []

1417+resolveTC def mvok depth top fn ist

1381−

1418+ = do hs <- get_holes

1419+ resTC' [] def hs depth top fn ist

1420+

1382−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

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

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

1423+resTC' tcs defaultOn topholes depth topg fn ist

1385− = do compute

1424+ = do compute

1386− g <- goal

1425+ g <- goal

1426+ let argsok = tcArgsOK g topholes

1427+-- trace (show (g,hs,argsok,topholes)) $

1428+ if not argsok -- && not mvok)

1429+ then lift $ tfail $ CantResolve True topg

1430+ else do

1387 ptm <- get_term

1431 ptm <- get_term

1388 ulog <- getUnifyLog

1432 ulog <- getUnifyLog

1389 hs <- get_holes

1433 hs <- get_holes

@@ -1400,6 +1444,31 @@ resTC' tcs defaultOn depth topg fn ist

1400 let depth' = if scopeOnly then 2 else depth

1444 let depth' = if scopeOnly then 2 else depth

1401 blunderbuss t depth' stk (stk ++ insts)) True

1445 blunderbuss t depth' stk (stk ++ insts)) True

1402 where

1446 where

1447+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1448+ = True

1449+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1450+ = let (f, as) = unApply ty in

1451+ case f of

1452+ P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1453+ Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1454+ Nothing -> not $ any (isMeta hs) as

1455+ _ -> not $ any (isMeta hs) as

1456+

1457+ tcDetArgsOK i ds hs (x : xs)

1458+ | i `elem` ds = not (isMeta hs x) && tcDetArgsOK (i + 1) ds hs xs

1459+ | otherwise = tcDetArgsOK (i + 1) ds hs xs

1460+ tcDetArgsOK _ _ _ [] = True

1461+

1462+ isMeta :: [Name] -> Term -> Bool

1463+ isMeta ns (P _ n _) = n `elem` ns

1464+ isMeta _ _ = False

1465+

1466+ notHole hs (P _ n _, c)

1467+ | (P _ cn _, _) <- unApply c,

1468+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1469+ | Constant _ <- c = not (n `elem` hs)

1470+ notHole _ _ = True

1471+

1403 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1472 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1404 | otherwise = (fail "Can't resolve", show n)

1473 | otherwise = (fail "Can't resolve", show n)

1405

1474

@@ -1427,10 +1496,13 @@ resTC' tcs defaultOn depth topg fn ist

1427

1496

1428 blunderbuss t d stk [] = do -- c <- get_env

1497 blunderbuss t d stk [] = do -- c <- get_env

1429 -- ps <- get_probs

1498 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1499+ lift $ tfail $ CantResolve False topg

1431 blunderbuss t d stk (n:ns)

1500 blunderbuss t d stk (n:ns)

1432 | n /= fn && (n `elem` stk || tcname n)

1501 | n /= fn && (n `elem` stk || tcname n)

1502+ = tryCatch (resolve n d)

1503+ (\e -> case e of

1504+ CantResolve True _ -> lift $ tfail e

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1505+ _ -> blunderbuss t d stk ns)

1434 | otherwise = blunderbuss t d stk ns

1506 | otherwise = blunderbuss t d stk ns

1435

1507

1436 resolve n depth

1508 resolve n depth

@@ -1459,7 +1531,7 @@ resTC' tcs defaultOn depth topg fn ist

1459 let got = fst (unApply t)

1531 let got = fst (unApply t)

1460 let depth' = if tc' `elem` tcs

1532 let depth' = if tc' `elem` tcs

1461 then depth - 1 else depth

1533 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1534+ resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

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

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

1464 -- if there's any arguments left, we've failed to resolve

1536 -- if there's any arguments left, we've failed to resolve

1465 hs <- get_holes

1537 hs <- get_holes

@@ -1505,11 +1577,17 @@ case_ ind autoSolve ist fn tm = do

1505 else casetac (forget val)

1577 else casetac (forget val)

1506 when autoSolve solveAll

1578 when autoSolve solveAll

1507

1579

1580+tacN :: String -> Name

1581+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1582+

1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1583+runTactical :: FC -> Env -> Term -> ElabD ()

1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1584+runTactical fc env tm = do tm' <- eval tm

1585+ runTacTm tm'

1586+ return ()

1510 where

1587 where

1588+ eval tm = do ctxt <- get_context

1511− eval = normaliseAll ctxt env . finalise

1589+ return $ normaliseAll ctxt env (finalise tm)

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

1590+

1513 returnUnit = fmap fst $ get_type_val (Var unitCon)

1591 returnUnit = fmap fst $ get_type_val (Var unitCon)

1514

1592

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

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

@@ -1547,26 +1625,31 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1547 = do env <- get_env

1625 = do env <- get_env

1548 fmap fst . get_type_val $ reflectEnv env

1626 fmap fst . get_type_val $ reflectEnv env

1549 | n == tacN "prim__Fail", [_a, errs] <- args

1627 | n == tacN "prim__Fail", [_a, errs] <- args

1628+ = do errs' <- eval errs

1550− = do parts <- reifyReportParts (eval errs)

1629+ parts <- reifyReportParts errs'

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

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

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

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

1553 = return tm

1632 = return tm

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

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

1555− = do let first' = eval first

1634+ = do first' <- eval first

1556 res <- runTacTm first'

1635 res <- runTacTm first'

1557− let next = eval (App andThen res)

1636+ next <- eval (App andThen res)

1558 runTacTm next

1637 runTacTm next

1559 | n == tacN "prim__Try", [_a, first, alt] <- args

1638 | n == tacN "prim__Try", [_a, first, alt] <- args

1560− = do let first' = eval first

1639+ = do first' <- eval first

1561− let alt' = eval alt

1640+ alt' <- eval alt

1562 try' (runTacTm first') (runTacTm alt') True

1641 try' (runTacTm first') (runTacTm alt') True

1563 | n == tacN "prim__Fill", [raw] <- args

1642 | n == tacN "prim__Fill", [raw] <- args

1564 = do raw' <- reifyRaw raw

1643 = do raw' <- reifyRaw raw

1565 apply raw' []

1644 apply raw' []

1566 returnUnit

1645 returnUnit

1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

1646+ | n == tacN "prim__Gensym", [hint] <- args

1647+ = do hintStr <- eval hint

1648+ case hintStr of

1649+ Constant (Str h) -> do

1568− = do n <- getNameFrom (sMN 0 hint)

1650+ n <- getNameFrom (sMN 0 h)

1569− fmap fst $ get_type_val (reflectName n)

1651+ fmap fst $ get_type_val (reflectName n)

1652+ _ -> fail "no hint"

1570 | n == tacN "prim__Claim", [n, ty] <- args

1653 | n == tacN "prim__Claim", [n, ty] <- args

1571 = do n' <- reifyTTName n

1654 = do n' <- reifyTTName n

1572 ty' <- reifyRaw ty

1655 ty' <- reifyRaw ty

@@ -1596,6 +1679,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1596 Just name -> fmap Just $ reifyTTName name

1679 Just name -> fmap Just $ reifyTTName name

1597 intro n

1680 intro n

1598 returnUnit

1681 returnUnit

1682+ | n == tacN "prim__DeclareType", [decl] <- args

1683+ = do (RDeclare n args res) <- reifyTyDecl decl

1684+ ctxt <- get_context

1685+ let mkPi arg res = RBind (argName arg)

1686+ (Pi Nothing (argTy arg) (RUType AllTypes))

1687+ res

1688+ rty = foldr mkPi res args

1689+ (checked, ty') <- lift $ check ctxt [] rty

1690+ case normaliseAll ctxt [] (finalise ty') of

1691+ TType _ -> lift . tfail . InternalMsg $

1692+ show checked ++ " is not a type: it's " ++ show ty'

1693+ _ -> return ()

1694+ case lookupDefExact n ctxt of

1695+ Just _ -> lift . tfail . InternalMsg $

1696+ show n ++ " is already defined."

1697+ Nothing -> return ()

1698+ let decl = TyDecl Ref checked

1699+ ctxt' = addCtxtDef n decl ctxt

1700+ set_context ctxt'

1701+ updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :

1702+ new_tyDecls e }

1703+ aux <- getAux

1704+ returnUnit

1599 | n == tacN "prim__Debug", [ty, msg] <- args

1705 | n == tacN "prim__Debug", [ty, msg] <- args

1600 = do let msg' = fromTTMaybe msg

1706 = do let msg' = fromTTMaybe msg

1601 case msg' of

1707 case msg' of

@@ -1850,6 +1956,7 @@ runTac autoSolve ist perhapsFC fn tac

1850 Just fc ->

1956 Just fc ->

1851 do fill $ reflectFC fc

1957 do fill $ reflectFC fc

1852 solve

1958 solve

1959+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

1853 runT x = fail $ "Not implemented " ++ show x

1960 runT x = fail $ "Not implemented " ++ show x

1854

1961

1855 runReflected t = do t' <- reify ist t

1962 runReflected t = do t' <- reify ist t

@@ -2361,7 +2468,7 @@ reflectTTQuote unq (P nt n t)

2361reflectTTQuote unq (V n)

2468reflectTTQuote unq (V n)

2362 = reflCall "V" [RConstant (I n)]

2469 = reflCall "V" [RConstant (I n)]

2363reflectTTQuote unq (Bind n b x)

2470reflectTTQuote unq (Bind n b x)

2364− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]

2471+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2365reflectTTQuote unq (App f x)

2472reflectTTQuote unq (App f x)

2366 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2473 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2367reflectTTQuote unq (Constant c)

2474reflectTTQuote unq (Constant c)

@@ -2378,7 +2485,7 @@ reflectRawQuote unq (Var n)

2378 | n `elem` unq = Var n

2485 | n `elem` unq = Var n

2379 | otherwise = reflCall "Var" [reflectName n]

2486 | otherwise = reflCall "Var" [reflectName n]

2380reflectRawQuote unq (RBind n b r) =

2487reflectRawQuote unq (RBind n b r) =

2381− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]

2488+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2382reflectRawQuote unq (RApp f x) =

2489reflectRawQuote unq (RApp f x) =

2383 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2490 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2384reflectRawQuote unq RType = Var (reflm "RType")

2491reflectRawQuote unq RType = Var (reflm "RType")

@@ -2436,27 +2543,27 @@ reflectNameQuotePattern _ -- for all other names, match any

2436 solve

2543 solve

2437

2544

2438reflectBinder :: Binder Term -> Raw

2545reflectBinder :: Binder Term -> Raw

2439−reflectBinder = reflectBinderQuote reflectTTQuote []

2546+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2440−

2547+

2441−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2548+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2442−reflectBinderQuote q unq (Lam t)

2549+reflectBinderQuote q ty unq (Lam t)

2443− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2550+ = reflCall "Lam" [Var ty, q unq t]

2444−reflectBinderQuote q unq (Pi _ t k)

2551+reflectBinderQuote q ty unq (Pi _ t k)

2445− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2552+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2446−reflectBinderQuote q unq (Let x y)

2553+reflectBinderQuote q ty unq (Let x y)

2447− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2554+ = reflCall "Let" [Var ty, q unq x, q unq y]

2448−reflectBinderQuote q unq (NLet x y)

2555+reflectBinderQuote q ty unq (NLet x y)

2449− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2556+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2450−reflectBinderQuote q unq (Hole t)

2557+reflectBinderQuote q ty unq (Hole t)

2451− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2558+ = reflCall "Hole" [Var ty, q unq t]

2452−reflectBinderQuote q unq (GHole _ t)

2559+reflectBinderQuote q ty unq (GHole _ t)

2453− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2560+ = reflCall "GHole" [Var ty, q unq t]

2454−reflectBinderQuote q unq (Guess x y)

2561+reflectBinderQuote q ty unq (Guess x y)

2455− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2562+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2456−reflectBinderQuote q unq (PVar t)

2563+reflectBinderQuote q ty unq (PVar t)

2457− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2564+ = reflCall "PVar" [Var ty, q unq t]

2458−reflectBinderQuote q unq (PVTy t)

2565+reflectBinderQuote q ty unq (PVTy t)

2459− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2566+ = reflCall "PVTy" [Var ty, q unq t]

2460

2567

2461mkList :: Raw -> [Raw] -> Raw

2568mkList :: Raw -> [Raw] -> Raw

2462mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2569mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2603,11 +2710,15 @@ reflectErr (NotInjective t1 t2 t3) =

2603 , reflect t2

2710 , reflect t2

2604 , reflect t3

2711 , reflect t3

2605 ]

2712 ]

2606−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2713+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2714+reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

2607reflectErr (CantResolveAlts ss) =

2715reflectErr (CantResolveAlts ss) =

2608 raw_apply (Var $ reflErrName "CantResolveAlts")

2716 raw_apply (Var $ reflErrName "CantResolveAlts")

2609 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2717 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2610reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2718reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2719+reflectErr (NoEliminator str t)

2720+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2721+ reflect t]

2611reflectErr UniverseError = Var $ reflErrName "UniverseError"

2722reflectErr UniverseError = Var $ reflErrName "UniverseError"

2612reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2723reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2613reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2724reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2748,6 +2859,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

2748 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2859 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2749reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2860reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2750

2861

2862+reifyTyDecl :: Term -> ElabD RTyDecl

2863+reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2864+ | n == tacN "Declare" =

2865+ do tyN' <- reifyTTName tyN

2866+ args' <- case unList args of

2867+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2868+ Just xs -> mapM reifyRArg xs

2869+ ret' <- reifyRaw ret

2870+ return $ RDeclare tyN' args' ret'

2871+ where reifyRArg :: Term -> ElabD RArg

2872+ reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2873+ | n == tacN "Explicit" = liftM2 RExplicit

2874+ (reifyTTName argN)

2875+ (reifyRaw argTy)

2876+ | n == tacN "Implicit" = liftM2 RImplicit

2877+ (reifyTTName argN)

2878+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2879+ (reifyTTName argN)

2880+ (reifyRaw argTy)

2881+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2882+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2883+

2751envTupleType :: Raw

2884envTupleType :: Raw

2752envTupleType

2885envTupleType

2753 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2886 = 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 }

@@ -1241,7 +1241,7 @@ instance (Binary t) => Binary (PDecl' t) where

1241 put x10

1242 put x11

1243 put x12

1244− PClass x1 x2 x3 x4 x5 x6 x7 x8

1244+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

1245 -> do putWord8 7

1246 put x1

1247 put x2

@@ -1251,6 +1251,7 @@ instance (Binary t) => Binary (PDecl' t) where

1251 put x6

1252 put x7

1253 put x8

1254+ put x9

1254 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1255 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1255 do putWord8 8

1256 do putWord8 8

1256 put x1

1257 put x1

@@ -1352,7 +1353,8 @@ instance (Binary t) => Binary (PDecl' t) where

1352 x6 <- get

1353 x6 <- get

1353 x7 <- get

1354 x7 <- get

1354 x8 <- get

1355 x8 <- get

1356+ x9 <- get

1355− return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1357+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

1356 8 -> do x1 <- get

1358 8 -> do x1 <- get

1357 x2 <- get

1359 x2 <- get

1358 x3 <- get

1360 x3 <- get

@@ -1424,7 +1426,7 @@ instance Binary Using where

1424 _ -> error "Corrupted binary data for Using"

1426 _ -> error "Corrupted binary data for Using"

1425

1427

1426instance Binary SyntaxInfo where

1428instance Binary SyntaxInfo where

1427− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1429+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

1428 = do put x1

1430 = do put x1

1429 put x2

1431 put x2

1430 put x3

1432 put x3

@@ -1440,7 +1442,7 @@ instance Binary SyntaxInfo where

1440 x5 <- get

1442 x5 <- get

1441 x6 <- get

1443 x6 <- get

1442 x7 <- get

1444 x7 <- get

1443− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)

1445+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

1444

1446

1445instance (Binary t) => Binary (PClause' t) where

1447instance (Binary t) => Binary (PClause' t) where

1446 put x

1448 put x

@@ -2077,19 +2079,21 @@ instance (Binary t) => Binary (PArg' t) where

2077

2079

2078

2080

2079instance Binary ClassInfo where

2081instance Binary ClassInfo where

2080− put (CI x1 x2 x3 x4 x5 _)

2082+ put (CI x1 x2 x3 x4 x5 _ x6)

2081 = do put x1

2083 = do put x1

2082 put x2

2084 put x2

2083 put x3

2085 put x3

2084 put x4

2086 put x4

2085 put x5

2087 put x5

2088+ put x6

2086 get

2089 get

2087 = do x1 <- get

2090 = do x1 <- get

2088 x2 <- get

2091 x2 <- get

2089 x3 <- get

2092 x3 <- get

2090 x4 <- get

2093 x4 <- get

2091 x5 <- get

2094 x5 <- get

2095+ x6 <- get

2092− return (CI x1 x2 x3 x4 x5 [])

2096+ return (CI x1 x2 x3 x4 x5 [] x6)

2093

2097

2094instance Binary OptInfo where

2098instance Binary OptInfo where

2095 put (Optimise x1 x2)

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

@@ -78,7 +78,7 @@ prove opt ctxt lit n ty

78 putIState (i { proof_list = (n, prf) : proofs })

79 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

80 logLvl 3 (show tree)

81− (ptm, pty) <- recheckC (fileFC "proof") [] tm

81+ (ptm, pty) <- recheckC (fileFC "proof") id [] tm

82 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

83 "Expected type:" ++ show ty)

84 case converts ctxt [] ty pty of

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/quasiquote001/expected+2−2

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

1(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))

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

3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))

4--------------

5−(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))

5+(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))

test/records001/test011.idr+5−5

@@ -22,9 +22,9 @@ person = MkPerson "Fred" 30

22main : IO ()

23main = do let x = record { name = "foo",

24 more_things = reverse ["a","b"] } testFoo

25− print $ name x

25+ printLn $ name x

26− print $ name person

26+ printLn $ name person

27− print $ things x

27+ printLn $ things x

28− print $ more_things x

28+ printLn $ more_things x

29− print $ age (record { age = 25 } person)

29+ printLn $ age (record { age = 25 } person)

30

test/records003/records003.idr+6−13

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

1record Person (age : Nat) where

2 constructor MkPerson

3 name : String

4−

5−--set_param_age : (age_in : Nat) -> Person age -> Person age_in

6−--set_param_age age_in (MkPerson {age=age} name) = MkPerson {age=age_in} name

7

4

8record Event where

5record Event where

9 constructor MkEvent

6 constructor MkEvent

@@ -18,9 +15,6 @@ record Meeting (year : Int) where

18new_organiser : String -> List (Meeting x) -> List (Meeting x)

15new_organiser : String -> List (Meeting x) -> List (Meeting x)

19new_organiser n = map (record { event->organiser->name = n })

16new_organiser n = map (record { event->organiser->name = n })

20

17

21−--set_param_year : (year_in : Int) -> Meeting year -> Meeting year_in

22−--set_param_year year_in (MkMeeting {year=year} event organiser) = MkMeeting {year=year_in} event organiser

23−

24next_year : Meeting x -> Meeting (x+1)

18next_year : Meeting x -> Meeting (x+1)

25next_year m = record { organiser->param_age

19next_year m = record { organiser->param_age

26 = record { organiser->param_age } m + 1,

20 = record { organiser->param_age } m + 1,

@@ -44,10 +38,9 @@ test : Meeting 2015

44test = next_year idm_gbg

38test = next_year idm_gbg

45

39

46main : IO ()

40main : IO ()

47−main = do print (record { event->organiser->name } test)

41+main = do printLn (record { event->organiser->name } test)

48− print (record { event->organiser->param_age } test)

42+ printLn (record { event->organiser->param_age } test)

49− print (record { event->organiser->param_age } idm_gbg)

43+ printLn (record { event->organiser->param_age } idm_gbg)

50− print (record { organiser->param_age } test)

44+ printLn (record { organiser->param_age } test)

51− print (record { organiser->param_age } idm_gbg)

45+ printLn (record { organiser->param_age } idm_gbg)

52− print (record { param_year } idm_gbg)

46+ printLn (record { param_year } idm_gbg)

53−

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

test/unique001/expected+1−1

@@ -17,4 +17,4 @@ with

17unique001b.idr:16:7:Borrowed name xs must not be used on RHS

18unique001c.idr:46:6:Unique name f is used more than once

19unique001d.idr:3:7:Borrowed name x must not be used on RHS

20−unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not

20+unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not