bbbe880 · Idris-dev · git.iko.soy

CHANGELOG+10−1

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

3434 command :elaborate-term for serialized terms.

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

3636* 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.

3847

3948New in 0.9.16:

4049--------------

Setup.hs+9−2

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

5757 Just False -> False

5858 Nothing -> True

5959

60+execOnly :: S.ConfigFlags -> Bool

61+execOnly flags =

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

63+ Just True -> True

64+ Just False -> False

65+ Nothing -> True

66+

6067isRelease :: S.ConfigFlags -> Bool

6168isRelease flags =

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

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

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

177184 return (Just buildinfo, [])

178185

179−idrisBuild _ flags _ local = do

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

180187 buildStdLib

181188 buildRTS

182189 where

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

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

200207-- Copy/Install

201208

202−idrisInstall verbosity copy pkg local = do

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

203210 installStdLib

204211 installRTS

205212 where

benchmarks/quasigroups/Main.idr+2−2

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

1414 Left err => putStrLn err

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

1616 putStrLn "Got board:"

17− print board

17+ printLn board

1818 putStrLn "Solving..."

1919 case fillBoard board legal of

2020 Nothing => putStrLn "No solution found"

2121 Just (solved ** _) => do

2222 putStrLn "Solution found:"

23− print solved

23+ printLn solved

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

benchmarks/trivial/sortvec.idr+2−3

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

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

1414

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

16−mkSortVec Z = return []

16+mkSortVec Z = return []

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

1818

1919main : IO ()

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

2121-- let arg = "2000"

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

2323 putStrLn "Made vector"

24− print (vsort vec)

25−

24+ printLn (vsort vec)

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

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

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

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

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

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

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

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

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

1313 exec_db_v2 stmt -- execute the prepared query

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

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

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

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

1717 close_db db -- close the datbase

1818 return ()

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

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

2323 let x = (fst sql)

2424 let list = (snd sql)

25− liftIO(print x)

25+ liftIO(printLn x)

2626 stmt <- (prepare_db db x)

2727 bindMulti stmt list

2828 exec_db_v2 stmt

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

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

3636 let x = (fst sql)

3737 let list = (snd sql)

38− liftIO(print x)

38+ liftIO(printLn x)

3939 stmt <- (prepare_db db x)

4040 bindMulti stmt list

4141 exec_db_v2 stmt

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

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

4949 let x = (fst sql)

5050 let list = (snd sql)

51− liftIO(print x)

51+ liftIO(printLn x)

5252 stmt <- (prepare_db db x)

5353 bindMulti stmt list

5454 exec_db_v2 stmt

5555 res <- toList_v1 db

56− liftIO(print res)

56+ liftIO(printLn res)

5757 finalize_db stmt

5858 close_db db

5959 return ()

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

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

6565 let x = (fst sql)

6666 let list = (snd sql)

67− liftIO(print x)

67+ liftIO(printLn x)

6868 stmt <- (prepare_db db x)

6969 bindMulti stmt list

7070 exec_db_v2 stmt

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

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

7979 let x = (fst sql)

8080 let list = (snd sql)

81− liftIO(print x)

81+ liftIO(printLn x)

8282 stmt <- (prepare_db db x)

8383 bindMulti stmt list

8484 exec_db_v2 stmt

8585 res <- toList_v1 db

86− liftIO(print res)

86+ liftIO(printLn res)

8787 finalize_db stmt

8888 close_db db

8989 return ()

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

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

9595 let x = (fst sql)

9696 let list = (snd sql)

97− liftIO(print x)

97+ liftIO(printLn x)

9898 stmt <- (prepare_db db x)

9999 bindMulti stmt list

100100 exec_db_v2 stmt

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

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

109109 let x = (fst sql)

110110 let list = (snd sql)

111− liftIO(print x)

111+ liftIO(printLn x)

112112 stmt <- (prepare_db db x)

113113 bindMulti stmt list

114114 exec_db_v2 stmt

115115 res <- toList_v1 db

116− liftIO(print res)

116+ liftIO(printLn res)

117117 finalize_db stmt

118118 close_db db

119119 return ()

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

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

124124 let x = (fst sql)

125125 let list = (snd sql)

126− liftIO(print x)

126+ liftIO(printLn x)

127127 stmt <- (prepare_db db x)

128128 bindMulti stmt list

129129 exec_db_v2 stmt

130130 res <- toList_v1 db

131− liftIO(print res)

131+ liftIO(printLn res)

132132 finalize_db stmt

133133 close_db db

134134 return ()

idris.cabal+9

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

289289 test/reg058/run

290290 test/reg058/*.idr

291291 test/reg058/expected

292+ test/reg059/run

293+ test/reg059/*.idr

294+ test/reg059/expected

292295

293296 test/basic001/run

294297 test/basic001/*.idr

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

658661 Default: False

659662 manual: True

660663

664+Flag execonly

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

666+ Default: False

667+ manual: True

668+

661669Library

662670 hs-source-dirs: src

663671 Exposed-modules:

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

725733 , Idris.ProofSearch

726734 , Idris.Prover

727735 , Idris.Providers

736+ , Idris.Reflection

728737 , Idris.REPL

729738 , Idris.REPLParser

730739 , Idris.Transforms

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

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

66%access public

77

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

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

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

1010 ||| Get the context

1111 get : m s

1212 ||| Write a new context/output

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

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

5656

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

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

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

6162 return (a, f' w)

6263

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

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

146146isEmptySizeZero Empty p = Refl

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

148148

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

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

150150emptyHeapValid = Refl

151151

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

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

182182 does seem to work correctly!

183183main : IO ()

184184main = do

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

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

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

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

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

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

188188 return ()

189189-}

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

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

3636 eq (f a) (f b)

3737

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

39−minimum x y with (order x y)

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

4040 | Left _ = x

4141 | Right _ = y

4242

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

44−maximum x y with (order x y)

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

4545 | Left _ = y

4646 | Right _ = x

4747

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

103103decideLTE Z y = Yes LTEZero

104104decideLTE (S x) Z = No zeroNeverGreater

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

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

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

107107 | No _ with (decideLTE x y)

108108 | Yes nLTEm = Yes (LTESucc nLTEm)

109109 | No nGTm = No (ltesuccinjective nGTm)

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

122122instance Ordered Nat LTE where

123123 order Z n = Left LTEZero

124124 order m Z = Right LTEZero

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

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

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

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

128128

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

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

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

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

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

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

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

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

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

275277 show UniverseError = "UniverseError"

276278 show ProgramLineComment = "ProgramLineComment"

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

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

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

44import System

55import Control.IOExcept

66

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

99

1010instance Handler (Exception a) Maybe where

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

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

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

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

3030raise err = call $ Raise err

3131

3232

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

3939

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

4141-- handler can be introduced mid interpretation?

42−

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

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

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

4343putStr s = call $ PutStr s

4444

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

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

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

48+

4549||| Write a character to standard output.

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

4751putChar c = call $ PutCh c

4852

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

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

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

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

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

55+putCharLn c = putStrLn (singleton c)

5256

5357||| Read a string from standard input.

5458getStr : { [STDIO] } Eff String

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

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

44import System

55import Control.IOExcept

66

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

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

99

1010instance Handler (Exception a) Maybe where

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

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2626EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

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

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

3030raise err = call $ Raise err

3131

3232

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

3939

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

4141-- handler can be introduced mid interpretation?

42−

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

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

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

417417

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

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

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

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

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

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

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

422422

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

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

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

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

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

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

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

427427

428428instance Quotable TTName TT where

429429 quotedTy = `(TTName)

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

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

2929 | NoTypeDecl TTName

3030 | NotInjective TT TT TT

3131 | CantResolve TT

32+ | InvalidTCArg TTName TT

3233 | CantResolveAlts (List TTName)

3334 | IncompleteTerm TT

35+ | NoEliminator String TT

3436 | UniverseError

3537 | ProgramLineComment

3638 | Inaccessible TTName

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

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

88import Prelude.Monad

99import Language.Reflection

1010

11+data Arg : Type where

12+ Explicit : TTName -> Raw -> Arg

13+ Implicit : TTName -> Raw -> Arg

14+ Constraint : TTName -> Raw -> Arg

15+

16+data TyDecl : Type where

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

18+

1119abstract

1220data Tactical : Type -> Type where

1321 -- obligatory control stuff

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

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

4048 prim__Intro : Maybe TTName -> Tactical ()

4149

50+ prim__DeclareType : TyDecl -> Tactical ()

51+

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

4353

54+

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

4556-- Public API

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

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

117128rewriteWith : Raw -> Tactical ()

118129rewriteWith rule = prim__Rewrite rule

119130

131+declareType : TyDecl -> Tactical ()

132+declareType decl = prim__DeclareType decl

133+

120134debug : Tactical a

121135debug = prim__Debug Nothing

122136

libs/prelude/Prelude.idr+15−5

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

442442putStrLn : String -> IO' ffi ()

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

444444

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

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

446446partial

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

448−print x = putStrLn (show x)

448+print x = putStr (show x)

449+

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

451+partial

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

453+printLn x = putStrLn (show x)

449454

450455||| Read one line of input from stdin

451456partial

452457getLine : IO' ffi String

453−getLine = prim_read

458+getLine = prim_read

454459

455460||| Write a single character to stdout

456461partial

457462putChar : Char -> IO ()

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

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

464+

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

466+partial

467+putCharLn : Char -> IO ()

468+putCharLn c = putStrLn (singleton c)

459469

460470||| Read a single character from stdin

461471partial

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

484494do_fopen : String -> String -> IO Ptr

485495do_fopen f m

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

487−

497+

488498||| Open a file

489499||| @ f the filename

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

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

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

316316

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

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

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

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

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

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

322322

libs/prelude/Prelude/Applicative.idr−4

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

1515 pure : a -> f a

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

1717

18−instance Applicative id where

19− pure a = a

20− f <*> a = f a

21−

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

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

2420 map g x = pure g <*> x

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

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

3131

3232||| Function composition

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

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

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

3535

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

3737||| @ f the function to flip

libs/prelude/Prelude/Functor.idr−2

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

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

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

2626

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

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

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

2626

27−instance Monad id where

28− a >>= f = f a

29−

3027||| Also called `join` or mu

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

3229flatten a = a >>= id

rts/idris_gc.c+3−14

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

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

113113 free(vm->heap.old);

114114

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

116− char* oldheap = 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;

115+ /* Allocate swap heap. */

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

128117

129118 VAL* root;

130119

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

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

140129 }

141130#endif

131+

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

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

144134

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

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

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

152142 }

153− vm->heap.old = oldheap;

154143

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

156145 HEAP_CHECK(vm)

rts/idris_heap.c+6−3

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

55#include <stddef.h>

66#include <stdio.h>

77

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

8+

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

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

911{

1012 char * mem = malloc(heap_size);

1113 if (mem == NULL) {

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

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

2830

2931 h->size = heap_size;

30− h->growth = heap_size;

32+ h->growth = growth;

3133

32− h->old = NULL;

34+ h->old = old;

3335}

3436

3537void free_heap(Heap * h) {

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

4042 }

4143}

4244

45+

4346// TODO: more testing

4447/******************** Heap testing ********************************************/

4548void heap_check_underflow(Heap * heap) {

rts/idris_heap.h+1−1

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

1414} Heap;

1515

1616

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

1818void free_heap(Heap * heap);

1919

2020

rts/idris_rts.c+1−1

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

2929 vm->valstack_base = valstack;

3030 vm->stack_max = valstack + stack_size;

3131

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

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

3333

3434 vm->ret = NULL;

3535 vm->reg1 = NULL;

samples/binary.idr+1−2

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

4141main : IO ()

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

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

44− print (adc n1 n2 b0)

44+ printLn (adc n1 n2 b0)

4545

4646

4747

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

9292 rewrite sym (plusZeroRightNeutral c) ;

9393 trivial;

9494}

95−

samples/interp-alt.idr+2−2

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

7777testFac = interp [] eFac 4

7878

7979main : IO ()

80−main = do print test

81− print testFac

80+main = do printLn test

81+ printLn testFac

samples/interp.idr+1−2

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

8888testFac = interp [] eFac 4

8989

9090main : IO ()

91−main = print testFac

92−

91+main = printLn testFac

samples/javaffi.idr+1−1

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

99main : IO ()

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

1111 res <- binom 49 6

12− print res

12+ printLn res

src/Idris/AbsSyntax.hs+47−23

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

360360addInstance int n i

361361 = do ist <- getIState

362362 case lookupCtxt n (idris_classes ist) of

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

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

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

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

365365 putIState $ ist { idris_classes = cs }

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

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

367367 putIState $ ist { idris_classes = cs }

368368 where addI i ins | int = i : ins

369369 | chaser n = ins ++ [i]

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

455455putIState :: IState -> Idris ()

456456putIState = put

457457

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

459+updateIState f = do i <- getIState

460+ putIState $ f i

461+

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

459463withContext ctx name dflt action = do

460464 ist <- getIState

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

547551addDeferred = addDeferred' Ref

548552addDeferredTyCon = addDeferred' (TCon 0 0)

549553

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

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

555+addDeferred' :: NameType

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

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

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

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

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

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

562+ -- allowed

563+ -> Idris ()

551564addDeferred' nt ns

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

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

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

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

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

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

10781091 = PClass doc info f

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

10801093 n

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

10821095 pDocs

1096+ fds

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

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

10851099 = PInstance doc argDocs info f

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

14661480

14671481-- Add implicit arguments in function calls

14681482addImplPat :: IState -> PTerm -> PTerm

1469−addImplPat = addImpl' True [] []

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

14701484

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

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

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

14731487

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

14761490

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

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

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

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

14791496addImpl = addImpl' False [] []

14801497

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

14821499-- and *not* inside a PHidden

14831500

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

1485−addImpl' inpat env infns ist ptm

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

1502+addImpl' inpat env infns imp_meths ist ptm

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

14871504 where

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

14891506 ai qq env ds (PRef fc f)

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

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

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

14951512 = let lt' = ai qq env ds lt

14961513 rt' = ai qq env ds rt

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

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

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

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

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

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

15321549 arity = getPArity ty in

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

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

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

15631580 = let ty' = ai qq env ds ty

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

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

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

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

15651584 PPi p n ty' sc'

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

15671586 = let r' = ai qq env ds r

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

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

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

15871606

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

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

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

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

15901609 = case lookupDef f (tt_ctxt ist) of

15911610 [] -> Right $ PPatvar fc f

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

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

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

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

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

15981617 else Right $ PPatvar fc f

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

16001619 imp _ = True

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

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

16091628 vname _ = False

16101629

1611−aiFn inpat expat qq ist fc f ds as

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

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

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

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

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

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

16181637 [] -> nh

16191638 x -> x

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

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

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

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

16251644 alts -> Right $

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

16281647 (insertImpl ns as)) alts

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

16301654 trimAlts [] alts = alts

16311655 trimAlts ns alts

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

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

16701694 PImp p True l n Placeholder :

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

16721696 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

16741698 case find n imps [] of

16751699 Just (tm, imps') ->

16761700 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+25−15

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

184184 idris_name :: Int,

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

186186 -- ^ Full application LHS on source line

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

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

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

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

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

191+ -- allowed

188192 idris_coercions :: [Name],

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

190194 syntax_rules :: SyntaxRules,

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

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

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

596600 Name -- Record name

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

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

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

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

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

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

601605 (Maybe Name) -- Optional constructor name

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

603607 SyntaxInfo -- Constructor SyntaxInfo

604608 -- ^ Record declaration

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

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

607610 [(Name, t)] -- constraints

608611 Name

609612 [(Name, t)] -- parameters

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

614+ [Name] -- determining parameters

611615 [PDecl' t] -- declarations

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

613617 -- class name, parameters, method declarations

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

640644-- For elaborator state

641645data EState = EState {

642646 case_decls :: [PDecl],

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

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

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

644649 }

645650

646−initEState = EState [] []

651+initEState :: EState

652+initEState = EState [] [] []

647653

648654type ElabD a = Elab' EState a

649655

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

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

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

703709declared (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

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

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

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

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

708714declared (PDSL n _) = [n]

709715declared (PSyntax _ _) = []

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

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

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

719725tldeclared (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

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

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

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

724730tldeclared (PParams _ _ ds) = []

725731tldeclared (PMutual _ ds) = concatMap tldeclared ds

726732tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

729735tldeclared _ = []

730736

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

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

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

741747defined (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

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

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

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

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

746752defined (PDSL n _) = [n]

747753defined (PSyntax _ _) = []

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

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

10431049 class_default_superclasses :: [PDecl],

10441050 class_params :: [Name],

1045− class_instances :: [Name] }

1051+ class_instances :: [Name],

1052+ class_determiners :: [Int] }

10461053 deriving Show

10471054{-!

10481055deriving instance Binary ClassInfo

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

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

12041211 syn_namespace :: [String],

12051212 no_imp :: [Name],

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

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

1215+ -- binders

12061216 decoration :: Name -> Name,

12071217 inPattern :: Bool,

12081218 implicitAllowed :: Bool,

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

12161226deriving instance Binary SyntaxInfo

12171227!-}

12181228

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

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

12201230

12211231expandNS :: SyntaxInfo -> Name -> Name

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

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

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

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

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

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

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

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

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

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

9191 put x

9292 put y

9393 put z

94− put (CantResolve t) = do putWord8 15

95− put t

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

95+ put t

9696 put (CantResolveAlts ns) = do putWord8 16

9797 put ns

9898 put (IncompleteTerm t) = do putWord8 17

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

146146 put x1

147147 put x2

148148 put x3

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

150+ put s

151+ put t

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

153+ put n

154+ put t

149155

150156 get = do i <- getWord8

151157 case i of

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

172178 13 -> fmap NoTypeDecl get

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

174180 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

181+ 15 -> fmap (CantResolve False) get

176182 16 -> fmap CantResolveAlts get

177183 17 -> fmap IncompleteTerm get

178184 18 -> return UniverseError

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

205211 x2 <- get

206212 x3 <- get

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

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

209221----- Generated by 'derive'

210222

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

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

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

8181 rnf (NotInjective x1 x2 x3)

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

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

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

84+ rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

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

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

8688 rnf UniverseError = ()

8789 rnf ProgramLineComment = ()

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

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

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

756756

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

758758try' t1 t2 proofSearch

759− = do s <- get

760− ps <- get_probs

761− ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

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

764− return $! v

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

766− if recoverableErr e1 then

767− do case runStateT t2 s of

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

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

770− then lift (tfail e1)

771− else lift (tfail e2)

772− else lift (tfail e1)

759+ = do s <- get

760+ ps <- get_probs

761+ ulog <- getUnifyLog

762+ case prunStateT 999999 False ps t1 s of

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

764+ return $! v

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

766+ if recoverableErr e1 then

767+ do case runStateT t2 s of

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

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

770+ then lift (tfail e1)

771+ else lift (tfail e2)

772+ else lift (tfail e1)

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

774774 = -- traceWhen r (show err) $

775775 r || proofSearch

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

782782 recoverableErr (ElabDebug _ _ _) = False

783783 recoverableErr _ = True

784784

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

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

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

792+ return $! v

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

794+ case runStateT (t2 e1) s of

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

796+ return $! v

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

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

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

786802tryWhen True a b = try a b

787803tryWhen False a b = a

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

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

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

682682 let tmt' = normalise ctxt env tmt

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

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

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

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

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

686686 case unApply tmt' of

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

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

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

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

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

719719 return scv'

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

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

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

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

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

723+ tmt'

723724 where scname = sMN 0 "scarg"

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

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

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

878879 ctxt = context ps

879880 ulog = unifylog ps

880881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

881883

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

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

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

889891 if newx || newy || ready ||

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

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

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

893− up (ns ++ v) ps

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

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

896+ up (ns ++ v') ps

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

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

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

src/Idris/Core/ProofTerm.hs+3

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

172172 else (t, False)

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

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

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

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

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

175178 updateSolved' xs t = (t, False)

176179

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

src/Idris/Core/TT.hs+38−14

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

155155 | WithFnType t

156156 | NoTypeDecl Name

157157 | NotInjective t t t

158− | CantResolve t

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

159+ t

160+ | InvalidTCArg Name t

159161 | CantResolveAlts [Name]

160162 | IncompleteTerm t

163+ | NoEliminator String t

161164 | UniverseError

162165 | UniqueError Universe Name

163166 | UniqueKindError Universe Name

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

231234 size (NoSuchVariable name) = size name

232235 size (NoTypeDecl name) = size name

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

234− size (CantResolve trm) = size trm

237+ size (CantResolve _ trm) = size trm

235238 size (NoRewriting trm) = size trm

236239 size (CantResolveAlts _) = 1

237240 size (IncompleteTerm trm) = size trm

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

246249

247250score :: Err -> Int

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

249−score (CantResolve _) = 20

252+score (CantResolve _ _) = 20

250253score (NoSuchVariable _) = 1000

251254score (ProofSearchFail e) = score e

252255score (CantSolveGoal _ _) = 100000

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

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

508511 concatMap (Map.toList) allns

509512

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

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

511514addAlist [] ctxt = ctxt

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

513516

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

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

935938instantiate :: TT n -> TT n -> TT n

936939instantiate e = subst 0 where

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

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

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

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

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

945949-- that has been substituted.

946950substV :: TT n -> TT n -> TT n

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

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

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

949954 | otherwise = V x

950955 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

10381043 -- substitution happens...)

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

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

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

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

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

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

11631171forget :: TT Name -> Raw

11641172forget tm = forgetEnv [] tm

11651173

1174+safeForget :: TT Name -> Maybe Raw

1175+safeForget tm = safeForgetEnv [] tm

1176+

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

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

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

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

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

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

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

1173−forgetEnv env (Constant c) = RConstant c

1174−forgetEnv env (TType i) = RType

1175−forgetEnv env (UType u) = RUType u

1176−forgetEnv env Erased = RConstant Forgot

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

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

1186+ | otherwise = Nothing

1187+safeForgetEnv env (Bind n b sc)

1188+ = do let n' = uniqueName n env

1189+ b' <- safeForgetEnvB env b

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

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)

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

1198+safeForgetEnv env (TType i) = Just RType

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

1200+safeForgetEnv env Erased = Just $ RConstant Forgot

11771201

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

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

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

101101 holeIn env f || f `elem` holes

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

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

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

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

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

106106 holeIn env f || f `elem` holes

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

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

111111 holeIn env f || f `elem` holes

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

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

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

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

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

116116 holeIn env f || f `elem` holes

src/Idris/Coverage.hs+1−1

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

2424-- provided explicitly from new clause generation.

2525mkPatTm :: PTerm -> Idris Term

2626mkPatTm t = do i <- getIState

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

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

2828 evalStateT (toTT (mapPT deNS timp)) 0

2929 where

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

src/Idris/DeepSeq.hs+6−6

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

149149 rnf x2 `seq`

150150 rnf x3 `seq`

151151 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` 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)

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

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

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

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

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

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

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

314314

315315instance NFData ClassInfo where

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

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

317317 = rnf x1 `seq`

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

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

319319

320320instance NFData OptInfo where

321321 rnf (Optimise x1 x2)

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

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

354354

355355instance NFData SyntaxInfo where

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

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

357357 = rnf x1 `seq`

358358 rnf x2 `seq`

359359 rnf x3 `seq`

360360 rnf x4 `seq`

361361 rnf x5 `seq`

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

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

src/Idris/Delaborate.hs+11−1

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

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

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

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

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

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

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

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

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

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

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

299303pprintErr' i (CantMatch t) =

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

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

302312pprintErr' i UniverseError = text "Universe inconsistency"

303313pprintErr' i (UniqueError NullType n)

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

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

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

5050

5151import Util.Pretty(pretty, text)

5252

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

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

5454

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

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

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

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

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

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

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

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

6061 let tty = pibind ps PType

6162 let constraint = PApp fc (PRef fc tn)

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

7576 let (methods, imethods)

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

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

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

7979 -- build instance constructor type

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

81− -- to elsewhere in the class declaration

8280 let cty = impbind ps $ conbind constraints

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

8482 constraint

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

8684 let ddecl = PDatadecl tn tty cons

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

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

86+ -- Elaborate the data declaration

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

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

89+ dets <- findDets cn fds

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

91+

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

90− logLvl 5 $ "Building functions"

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

92−-- ++ using syn }

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

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

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

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

95+

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

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

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

99+ -- Elaborate the the top level methods

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

101+

98102 -- add the default definitions

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

100104 addIBC (IBCClass tn)

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

130134

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

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

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

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

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

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

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

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

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

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

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

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

203207

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

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

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

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

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

207211 getMArgs _ = []

208212

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

210214 | otherwise = getMeth ms as x

211215

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

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

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

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

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

215219 lhsArgs [] _ = []

216220

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

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

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

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

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

220224 rhsArgs [] _ = []

221225

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

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

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

232236 toExp ns e sc = sc

237+

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

239+findDets n ns =

240+ do i <- getIState

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

242+ Just ty -> getDetPos 0 ns ty

243+ Nothing -> []

244+ where

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

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

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

248+ getDetPos _ _ _ = []

249+

250+

src/Idris/Elab/Clause.hs+44−32

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

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

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

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

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

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

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

459+ do setContext ctxt'

460+ processTacticDecls newDecls

461+ let lhs_tm = orderPats (getInferTerm lhs')

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

461463 OK _ -> return True

462464 err -> return False

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

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

547549 = do let tcgen = Dictionary `elem` opts

548550 i <- get

549− let lhs = addImpl i lhs_in

551+ let lhs = addImpl [] i lhs_in

550552 b <- checkPossible info fc tcgen fname lhs_in

551553 case b of

552554 True -> tclift $ tfail (At fc

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

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

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

581583

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

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

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

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

586− probs <- get_probs

587− inj <- get_inj

588− return (res, probs, inj))

589−

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

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

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

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

588+ probs <- get_probs

589+ inj <- get_inj

590+ return (res, probs, inj))

591+ setContext ctxt'

592+ processTacticDecls newDecls

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

591594

592595 let lhs_tm = orderPats (getInferTerm lhs')

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

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

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

602605 (clhs_c, clhsty) <- if not inf

603− then recheckC fc [] lhs_tm

606+ then recheckC fc id [] lhs_tm

604607 else return (lhs_tm, lhs_ty)

605608 let clhs = normalise ctxt [] clhs_c

606609 let borrowed = borrowedNames [] clhs

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

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

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

655658 logLvl 5 "STARTING CHECK"

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

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

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

658661 (do pbinds ist lhs_tm

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

660663 setNextName

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

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

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

665+ errAt "right hand side of " fname

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

663667 errAt "right hand side of " fname

664668 (erun fc $ psolve lhs_tm)

665669 hs <- get_holes

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

668672 tt <- get_term

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

670674 probs <- get_probs

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

672−

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

676+ setContext ctxt'

677+ processTacticDecls newDecls

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

674679

675680 logLvl 5 "DONE CHECK"

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

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

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

679− def' <- checkDef fc defer

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

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

681686 addDeferred def''

682687 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

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

696701

697702 (crhs, crhsty) <- if not inf

698− then recheckC_borrowing True borrowed fc [] rhs'

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

699704 else return (rhs', clhsty)

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

701706 ctxt <- getContext

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

812817 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

824+ setContext ctxt'

825+ processTacticDecls newDecls

819826 let lhs_tm = orderPats (getInferTerm lhs')

820827 let lhs_ty = getInferType lhs'

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

822829 let static_names = getStaticNames i lhs_tm

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

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

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

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

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

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

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

829836 -- Elaborate wval in this context

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

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

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

832839 (bindTyArgs PVTy bargs infP) initEState

833840 (do pbinds i lhs_tm

834841 setNextName

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

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

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

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

838845 erun fc $ psolve lhs_tm

839846 tt <- get_term

840− return (tt, d, is))

841− def' <- checkDef fc defer

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

848+ setContext ctxt'

849+ processTacticDecls newDecls

850+ def' <- checkDef fc iderr defer

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

843852 addDeferred def''

844853 mapM_ (elabCaseBlock info opts) is

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

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

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

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

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

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

898907 addIBC (IBCImp wname)

899908 addIBC (IBCStatic wname)

900909

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

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

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

903912 addDeferred def''

904913

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

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

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

925934 i <- getIState

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

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

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

928937 (do pbinds i lhs_tm

929938 setNextName

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

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

931940 psolve lhs_tm

932941 tt <- get_term

933− return (tt, d, is))

934− def' <- checkDef fc defer

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

943+ setContext ctxt'

944+ processTacticDecls newDecls

945+

946+ def' <- checkDef fc iderr defer

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

936948 addDeferred def''

937949 mapM_ (elabCaseBlock info opts) is

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

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

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

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

941953 where

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

215215 Idris (Name, Type)

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

217217 = do checkUndefined fc n

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

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

219220 ctxt <- getContext

220221 let cty' = normalise ctxt [] cty

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

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

224225 tyIs n cty'

225226

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

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

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

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

229230

src/Idris/Elab/Instance.hs+52−13

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

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

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

7777 case expn of

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

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

7979 (class_instances ci)

8080 addInstance intInst n iname

8181 Just _ -> addInstance intInst n iname

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

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

136136 iLOG (show idecls)

137137 mapM_ (rec_elabDecl info EAll info) idecls

138+ ist <- getIState

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

138140 addIBC (IBCInstance intInst n iname)

139141

140142 where

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

167169 = do ty' <- addUsingConstraints syn fc t

168170 -- TODO think: something more in info?

169171 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

172+ let ty = addImpl [] i ty'

171173 ctxt <- getContext

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

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

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

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

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

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

177+ setContext ctxt'

178+ processTacticDecls newDecls

175179 ctxt <- getContext

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

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

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

179183

180− findOverlapping i t n

184+ findOverlapping i dets t n

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

182186 | otherwise

183187 = case lookupTy n (tt_ctxt i) of

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

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

186− case matchClause i tret' tret of

187− Right ms -> Just tret'

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

189− Right ms -> Just tret'

190− Left _ -> Nothing

190+ case matchArgs i dets tret' tret of

191+ Right _ -> Just tret'

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

193+ Right _ -> Just tret'

194+ Left _ -> Nothing

191195 _ -> Nothing

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

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

194198 getRetType (PPi _ _ _ sc) = getRetType sc

195199 getRetType t = t

196200

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+

197211 mkMethApp (n, _, _, ty)

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

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

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

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

265279 = decorate ns iname m == decorate ns iname m'

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

3030 SyntaxInfo -> -- ^ Constructor SyntaxInfo

3131 Idris ()

3232elabRecord 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

3434 -- Type constructor

35− let tycon = generateTyCon params

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

35+ let tycon = generateTyConType params

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

3737

3838 -- Data constructor

3939 dconName <- generateDConName cname

40− let dcon = generateDCon params fields

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

40+ let dconTy = generateDConType params fields

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

4242

4343 -- 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, [])]

4545 elabData info rsyn doc [] fc opts datadecl

4646

4747 i <- getIState

4848

49− -- The elaborated constructor for the data declaration

50− ttCons <-

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

50+ ttConsTy <-

5151 case lookupTyExact dconName (tt_ctxt i) of

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

5454

5555 -- The arguments to the constructor

56− let constructorArgs = getArgTys ttCons

56+ let constructorArgs = getArgTys ttConsTy

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

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

5959

6060 -- The parameters for elaboration with their documentation

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

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

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

6263

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

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

6566

6667 -- 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−

69− -- Build projection functions

70− elabProj dconName fieldsForElab

71− -- Build update functions

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

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

69+ -- Build and elaborate projection functions

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

74+ -- Build and elaborate update functions

75+ elabUp dconName updaters

7376 where

7477 -- | Generates a type constructor.

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

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

77− generateTyCon [] = PType

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

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

80+ generateTyConType [] = PType

7881

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

8083 generateDConName :: Maybe Name -> Idris Name

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

8891 Nothing -> return n

8992

9093 -- | Generates the data constructor type.

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

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

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

94− generateDCon [] [] = target

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

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

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

97+ generateDConType [] [] = target

9598

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

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

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

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

101+ asPRefArg p n = asArg p (nsroot n) $ PRef fc (nsroot n)

99102

100103 -- | The target for the constructor and projection functions. Also the source of the update functions.

101104 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]

103106

104107 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.

105108 placeholderArg :: Plicity -> Name -> PArg

@@ -127,50 +130,57 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

127130 fieldTerms :: [PTerm]

128131 fieldTerms = [t | (_, _, t) <- fields]

129132

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−

138133 -- Delabs the TT to PTerm

139134 -- This is not good.

140135 -- However, for machine generated implicits, there seems to be no PTerm available.

141136 -- Is there a better way to do this without building the setters and getters as TT?

142137 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)

144−

145− free_name :: Name -> Name

146− free_name (UN n) = sUN ("free_" ++ str n)

147− free_name (MN i n) = sMN i ("free_" ++ str n)

148− free_name (NS n s) = NS (free_name n) s

149− free_name n = n

150−

151− zip' :: 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− zip' i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zip' i rest [])

138+ freeField i arg = let nameInCons = fst arg -- The name as it appears in the constructor

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+ freeName :: Name -> Name

146+ freeName (UN n) = sUN ("free_" ++ str n)

147+ freeName (MN i n) = sMN i ("free_" ++ str n)

148+ freeName (NS n s) = NS (freeName n) s

149+ freeName n = n

150+

151+ -- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.

152+ zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]

153+ zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')

154+ zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])

154155 where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring

155− zip' _ [] [] = []

156+ zipParams _ [] [] = []

156157

157− param_name :: Name -> Name

158− param_name (UN n) = sUN ("param_" ++ str n)

159− param_name (MN i n) = sMN i ("param_" ++ str n)

160− param_name (NS n s) = NS (param_name n) s

161− param_name n = n

158+ paramName :: Name -> Name

159+ paramName (UN n) = sUN ("param_" ++ str n)

160+ paramName (MN i n) = sMN i ("param_" ++ str n)

161+ paramName (NS n s) = NS (paramName n) s

162+ paramName n = n

162163

163164 -- | Elaborate the projection functions.

164165 elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

165166 elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

166167 elab = \(n, n', p, t, doc, i) ->

168+ -- Use projections in types

167169 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs] t

168170 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i

169171 in mapM_ elab fs

170172

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+

171181 -- | Elaborate the update functions.

172182 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]

174184 elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

175185 in mapM_ elab fs

176186

@@ -180,7 +190,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

180190

181191 -- | A map from a field name to the other fields it depends on.

182192 fieldDependencies :: [(Name, [Name])]

183− fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields]

193+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]

184194 where

185195 fieldDep :: Name -> PTerm -> (Name, [Name])

186196 fieldDep n t = ((nsroot n), fieldNames `intersect` allNamesIn t)

@@ -214,15 +224,15 @@ elabProjection :: ElabInfo ->

214224 Int -> -- ^ Argument Index

215225 Idris ()

216226elabProjection 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

218228

219229 let ty = generateTy

220− logLvl 4 $ "Type of " ++ show pname ++ ": " ++ show ty

230+ logLvl 1 $ "Type of " ++ show pname ++ ": " ++ show ty

221231

222232 let lhs = generateLhs

223− logLvl 4 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

233+ logLvl 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

224234 let rhs = generateRhs

225− logLvl 4 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

235+ logLvl 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

226236

227237 rec_elabDecl info EAll info ty

228238

@@ -278,23 +288,23 @@ elabUpdate :: ElabInfo ->

278288 Bool -> -- ^ Optional

279289 Idris ()

280290elabUpdate 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

282292

283293 let ty = generateTy

284− logLvl 4 $ "Type of " ++ show set_pname ++ ": " ++ show ty

294+ logLvl 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty

285295

286296 let lhs = generateLhs

287− logLvl 4 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

297+ logLvl 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

288298

289299 let rhs = generateRhs

290− logLvl 4 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

300+ logLvl 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

291301

292302 let clause = PClause fc set_pname lhs [] rhs []

293303

294304 idrisCatch (do rec_elabDecl info EAll info ty

295305 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])

296306 (\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

298308 else tclift $ tfail $ At fc (Elaborating "record update function" pname err))

299309 where

300310 -- | 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

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

56− ((lhs', dlhs, []), _) <-

56+ (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

5757 tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState

5858 (erun fc (buildTC i info ELHS [] (sUN "transform")

5959 (infTerm lhs)))

60+ setContext ctxt'

61+ processTacticDecls newDecls

6062 let lhs_tm = orderPats (getInferTerm lhs')

6163 let lhs_ty = getInferType lhs'

6264 let newargs = pvars i lhs_tm

6365

64− (clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm

66+ (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

6567 let clhs_tm = renamepats pnames clhs_tm_in

6668 logLvl 3 ("Transform LHS " ++ show clhs_tm)

6769

6870 let rhs = addImplBound i (map fst newargs) rhs_in

69− ((rhs', defer), _) <-

71+ ((rhs', defer, ctxt', newDecls), _) <-

7072 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

7173 (do pbinds i lhs_tm

7274 setNextName

73− erun fc (build i info ERHS [] (sUN "transform") rhs)

75+ (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

7476 erun fc $ psolve lhs_tm

7577 tt <- get_term

76− return (runState (collectDeferred Nothing tt) []))

77− (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

78+ let (rhs', defer) = runState (collectDeferred Nothing tt) []

79+ return (rhs', defer, ctxt', newDecls))

80+ setContext ctxt'

81+ processTacticDecls newDecls

82+

83+ (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'

7884 let crhs_tm = renamepats pnames crhs_tm_in

7985 logLvl 3 ("Transform RHS " ++ show crhs_tm)

8086

src/Idris/Elab/Type.hs+17−13

@@ -57,23 +57,25 @@ buildType info syn fc opts n ty' = do

5757 ctxt <- getContext

5858 i <- getIState

5959

60− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

60+ logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

6161 ty' <- addUsingConstraints syn fc ty'

6262 ty' <- addUsingImpls syn n fc ty'

63− let ty = addImpl i ty'

63+ let ty = addImpl (imp_methods syn) i ty'

6464

65− logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66− logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

65+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66+ logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

6767

68− ((tyT', defer, is), log) <-

69− tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

68+ (ElabResult tyT' defer is ctxt' newDecls, log) <-

69+ tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

71+ setContext ctxt'

72+ processTacticDecls newDecls

7173

7274 let tyT = patToImp tyT'

7375

7476 logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

7577

76− ds <- checkAddDef True False fc defer

78+ ds <- checkAddDef True False fc iderr defer

7779 -- if the type is not complete, note that we'll need to infer

7880 -- things later (for solving metavariables)

7981 when (not (null ds)) $ addTyInferred n

@@ -83,7 +85,7 @@ buildType info syn fc opts n ty' = do

8385 logLvl 5 $ "Rechecking"

8486 logLvl 6 $ show tyT

8587 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

86− (cty, ckind) <- recheckC fc [] tyT

88+ (cty, ckind) <- recheckC fc id [] tyT

8789

8890 -- record the implicit and inaccessible arguments

8991 i <- getIState

@@ -114,12 +116,14 @@ buildType info syn fc opts n ty' = do

114116 param_pos i ns t = []

115117

116118-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

118− FC -> FnOpts -> Name -> PTerm -> Idris Type

119+elabType :: ElabInfo -> SyntaxInfo

120+ -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

121+ -> FC -> FnOpts -> Name -> PTerm -> Idris Type

119122elabType = elabType' False

120123

121124elabType' :: Bool -> -- normalise it

122− ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

125+ ElabInfo -> SyntaxInfo ->

126+ Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

123127 FC -> FnOpts -> Name -> PTerm -> Idris Type

124128elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125129 n = liftname info n_in in -}

@@ -150,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

150154 -- Productivity checking now via checking for guarded 'Delay'

151155 let opts' = opts -- if corec then (Coinductive : opts) else opts

152156 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))]

154158 addIBC (IBCDef n)

155159 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

156160 addDeferred ds'

src/Idris/Elab/Utils.hs+23−15

@@ -22,31 +22,41 @@ import Debug.Trace

2222

2323import qualified Data.Map as Map

2424

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

2626

27−recheckC_borrowing uniq_check bs fc env t

27+recheckC_borrowing uniq_check bs fc mkerr env t

2828 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

2929 ctxt <- getContext

30− (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of

31− Error e -> tfail (At fc e)

30+ t' <- case safeForget t of

31+ Just ft -> return ft

32+ Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

33+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

34+ Error e -> tfail (At fc (mkerr e))

3235 OK x -> return x

3336 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

3437 addConstraints fc cs

3538 return (tm, ty)

3639

40+iderr :: Name -> Err -> Err

41+iderr _ e = e

3742

38−checkDef fc ns = checkAddDef False True fc ns

43+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]

44+ -> Idris [(Name, (Int, Maybe Name, Type))]

45+checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

3946

40−checkAddDef add toplvl fc [] = return []

41−checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

47+checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

48+ -> [(Name, (Int, Maybe Name, Type))]

49+ -> Idris [(Name, (Int, Maybe Name, Type))]

50+checkAddDef add toplvl fc mkerr [] = return []

51+checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)

4252 = do ctxt <- getContext

43− (t', _) <- recheckC fc [] t

53+ (t', _) <- recheckC fc (mkerr n) [] t

4454 when add $ do addDeferred [(n, (i, top, t, toplvl))]

4555 addIBC (IBCDef n)

46− ns' <- checkAddDef add toplvl fc ns

56+ ns' <- checkAddDef add toplvl fc mkerr ns

4757 return ((n, (i, top, t')) : ns')

4858

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

5060-- type

5161inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

5262inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

@@ -54,7 +64,7 @@ inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

5464 | otherwise = inaccessibleImps (i + 1) sc ins

5565inaccessibleImps _ _ _ = []

5666

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.

5868inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

5969inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

6070 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

@@ -74,10 +84,9 @@ elabCaseBlock info opts d@(PClauses f o n ps)

7484 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

7585 rec_elabDecl info EAll info (PClauses f opts' n ps )

7686

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

7888-- (i.e. - if we inferred any arguments that the user provided, make sure

7989-- they are the same!)

80−

8190checkInferred :: FC -> PTerm -> PTerm -> Idris ()

8291checkInferred fc inf user =

8392 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

@@ -92,9 +101,8 @@ checkInferred fc inf user =

92101 logLvl 10 $ "Checked match"

93102-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

94103

95−-- Return whether inferred term is different from given term

104+-- | Return whether inferred term is different from given term

96105-- (as above, but return a Bool)

97−

98106inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

99107inferredDiff fc inf user =

100108 do i <- getIState

src/Idris/Elab/Value.hs+11−6

@@ -56,25 +56,30 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam

5656elabValBind info aspat norm tm_in

5757 = do ctxt <- getContext

5858 i <- getIState

59− let tm = addImpl i tm_in

59+ let tm = addImpl [] i tm_in

6060 logLvl 10 (showTmImpls tm)

6161 -- try:

6262 -- * ordinary elaboration

6363 -- * elaboration as a Type

6464 -- * elaboration as a function a -> b

6565

66− ((tm', defer, is), _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP initEState

68− (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

66+ (ElabResult tm' defer is ctxt' newDecls, _) <-

67+ tclift (elaborate ctxt (sMN 0 "val") infP initEState

68+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

69+

70+ -- Extend the context with new definitions created

71+ setContext ctxt'

72+ processTacticDecls newDecls

73+

6974 let vtm = orderPats (getInferTerm tm')

7075

71− def' <- checkDef (fileFC "(input)") defer

76+ def' <- checkDef (fileFC "(input)") iderr defer

7277 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

7378 addDeferred def''

7479 mapM_ (elabCaseBlock info []) is

7580

7681 logLvl 3 ("Value: " ++ show vtm)

77− (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm

82+ (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

7883

7984 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

8085 else vtm_in

src/Idris/ElabDecls.hs+2−2

@@ -229,10 +229,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

229229 ninfo = case namespace info of

230230 Nothing -> info { namespace = Just [n] }

231231 Just ns -> info { namespace = Just (n:ns) }

232−elabDecl' what info (PClass doc s f cs n ps pdocs ds)

232+elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)

233233 | what /= EDefns

234234 = do iLOG $ "Elaborating class " ++ show n

235− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

235+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds

236236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237237 = do iLOG $ "Elaborating instance " ++ show n

238238 elabInstance info s doc argDocs what f cs n ps t expn ds

src/Idris/ElabTerm.hs+214−81

@@ -18,6 +18,7 @@ import Idris.Core.Typecheck (check, recheck)

1818import Idris.ErrReverse (errReverse)

1919import Idris.ElabQuasiquote (extractUnquotes)

2020import Idris.Elab.Utils

21+import Idris.Reflection

2122import qualified Util.Pretty as U

2223

2324import Control.Applicative ((<$>))

@@ -36,6 +37,32 @@ import Debug.Trace

3637data ElabMode = ETyDecl | ELHS | ERHS

3738 deriving Eq

3839

40+data ElabResult =

41+ ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

42+ , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

43+ -- ^ Information about new metavariables

44+ , resultCaseDecls :: [PDecl]

45+ -- ^ Deferred declarations as the meaning of case blocks

46+ , resultContext :: Context

47+ -- ^ The potentially extended context from new definitions

48+ , resultTyDecls :: [(Name, FC, [PArg], Type)]

49+ -- ^ Meta-info about the new type declarations

50+ }

51+

52+processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()

53+processTacticDecls info =

54+ forM_ info $ \(n, fc, impls, ty) ->

55+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

56+ logLvl 3 $ " It has impls " ++ show impls

57+ updateIState $ \i -> i { idris_implicits =

58+ addDef n impls (idris_implicits i) }

59+ addIBC (IBCImp n)

60+ ds <- checkDef fc 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+

3966-- Using the elaborator, convert a term in raw syntax to a fully

4067-- elaborated, typechecked term.

4168--

@@ -45,7 +72,7 @@ data ElabMode = ETyDecl | ELHS | ERHS

4572-- Also find deferred names in the term and their types

4673

4774build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

48− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

75+ ElabD ElabResult

4976build ist info emode opts fn tm

5077 = do elab ist info emode opts fn tm

5178 let tmIn = tm

@@ -64,7 +91,7 @@ build ist info emode opts fn tm

6491 mapM_ (\n -> when (n `elem` hs) $

6592 do focus n

6693 g <- goal

67− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

6895 (movelast n)) ivs

6996 ivs <- get_instances

7097 hs <- get_holes

@@ -72,7 +99,8 @@ build ist info emode opts fn tm

7299 mapM_ (\n -> when (n `elem` hs) $

73100 do focus n

74101 g <- goal

75− resolveTC True 7 g fn ist) ivs

102+ ptm <- get_term

103+ resolveTC True True 7 g fn ist) ivs

76104 tm <- get_term

77105 ctxt <- get_context

78106 probs <- get_probs

@@ -94,12 +122,13 @@ build ist info emode opts fn tm

94122 when tydecl (do update_term orderPats

95123 mkPat)

96124-- update_term liftPats)

97− EState is _ <- getAux

125+ EState is _ impls <- getAux

98126 tt <- get_term

99127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

100128 log <- getLog

101− if (log /= "") then trace log $ return (tm, ds, is)

102− else return (tm, ds, is)

129+ ctxt <- get_context

130+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

131+ else return (ElabResult tm ds is ctxt impls)

103132 where pattern = emode == ELHS

104133 tydecl = emode == ETyDecl

105134

@@ -114,7 +143,7 @@ build ist info emode opts fn tm

114143-- know about yet on the LHS of a pattern def)

115144

116145buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

117− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

146+ ElabD ElabResult

118147buildTC ist info emode opts fn tm

119148 = do -- set name supply to begin after highest index in tm

120149 let ns = allNamesIn tm

@@ -135,12 +164,13 @@ buildTC ist info emode opts fn tm

135164 -- unification

136165 when (not (null dots)) $

137166 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

167+ EState is _ impls <- getAux

139168 tt <- get_term

140169 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

141170 log <- getLog

142− if (log /= "") then trace log $ return (tm, ds, is)

143− else return (tm, ds, is)

171+ ctxt <- get_context

172+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

173+ else return (ElabResult tm ds is ctxt impls)

144174 where pattern = emode == ELHS

145175

146176-- return whether arguments of the given constructor name can be

@@ -183,9 +213,9 @@ goal_polymorphic =

183213 _ -> return True

184214 _ -> return False

185215

186−-- Returns the set of declarations we need to add to complete the definition

187−-- (most likely case blocks to elaborate)

188−

216+-- | Returns the set of declarations we need to add to complete the

217+-- definition (most likely case blocks to elaborate) as well as

218+-- declarations resulting from user tactic scripts (%runTactics)

189219elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

190220 ElabD ()

191221elab ist info emode opts fn tm

@@ -321,7 +351,7 @@ elab ist info emode opts fn tm

321351 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322352 _ -> elab' ina (Just fc) (PRef fc unitCon)

323353 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

324− = do g <- goal; resolveTC False 5 g fn ist

354+ = do g <- goal; resolveTC False False 5 g fn ist

325355 elab' ina fc (PResolveTC fc')

326356 = do c <- getNameFrom (sMN 0 "class")

327357 instanceArg c

@@ -540,7 +570,7 @@ elab ist info emode opts fn tm

540570 g <- goal

541571 hs <- get_holes

542572 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

543− then try (resolveTC True 7 g fn ist)

573+ then try (resolveTC True False 7 g fn ist)

544574 (movelast n)

545575 else movelast n)

546576 (ivs' \\ ivs)

@@ -700,7 +730,7 @@ elab ist info emode opts fn tm

700730 env <- get_env

701731 hs <- get_holes

702732 if all (\n -> not (n `elem` hs)) (freeNames g)

703− then try (resolveTC False 7 g fn ist)

733+ then try (resolveTC False False 7 g fn ist)

704734 (movelast n)

705735 else movelast n)

706736 (ivs' \\ ivs)

@@ -965,17 +995,14 @@ elab ist info emode opts fn tm

965995 elab' ina fc (PUnifyLog t) = do unifyLog True

966996 elab' ina fc t

967997 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

969999 = do -- First extract the unquoted subterms, replacing them with fresh

9701000 -- names in the quasiquoted term. Claim their reflections to be

9711001 -- an inferred type (to support polytypic quasiquotes).

1002+ finalTy <- goal

9721003 (t, unq) <- extractUnquotes 0 t

9731004 let unquoteNames = map fst unq

974− mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")

975− claim uqh RType

976− movelast uqh

977− claim uqn (Var uqh)) unquoteNames

978−

1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames

9791006

9801007 -- Save the old state - we need a fresh proof state to avoid

9811008 -- capturing lexically available variables in the quoted term.

@@ -1010,7 +1037,7 @@ elab ist info emode opts fn tm

10101037 letbind nTm (Var qTy) (Var qTm)

10111038

10121039 -- Fill out the goal type, if relevant

1013− case goal of

1040+ case goalt of

10141041 Nothing -> return ()

10151042 Just gTy -> do focus qTy

10161043 elabE (ina { e_qq = True }) fc gTy

@@ -1025,18 +1052,20 @@ elab ist info emode opts fn tm

10251052 env <- get_env

10261053 loadState

10271054 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1028−

1055+ isRaw = case unApply (normaliseAll ctxt env finalTy) of

1056+ (P _ n _, []) | n == reflm "Raw" -> True

1057+ _ -> False

10291058 case quoted of

10301059 Just q -> do ctxt <- get_context

10311060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

10321061 if pattern

1033− then do try' (reflectTTQuotePattern unquoteNames q')

1034− (reflectRawQuotePattern unquoteNames (forget q'))

1035− True

1036− else do try' (fill $ reflectTTQuote unquoteNames q')

1037− -- we forget q' instead of using q to ensure rechecking

1038− (fill $ reflectRawQuote unquoteNames (forget q'))

1039− True -- ignore errors like proof search does

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1064+ else reflectTTQuotePattern unquoteNames q'

1065+ else do if isRaw

1066+ then -- we forget q' instead of using q to ensure rechecking

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1068+ else fill $ reflectTTQuote unquoteNames q'

10401069 solve

10411070

10421071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

@@ -1077,8 +1106,8 @@ elab ist info emode opts fn tm

10771106 focus n

10781107 elab' ina (Just fc') tm

10791108 env <- get_env

1080− ctxt <- get_context

1081− runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)

1109+ runTactical (maybe fc' id fc) env (P Bound n' Erased)

1110+ EState _ _ todo <- getAux

10821111 solve

10831112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

10841113

@@ -1346,9 +1375,12 @@ findInstances :: IState -> Term -> [Name]

13461375findInstances ist t

13471376 | (P _ n _, _) <- unApply t

13481377 = case lookupCtxt n (idris_classes ist) of

1349− [CI _ _ _ _ _ ins] -> ins

1378+ [CI _ _ _ _ _ ins _] -> filter accessible ins

13501379 _ -> []

13511380 | otherwise = []

1381+ where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

1382+ Just (_, Hidden) -> False

1383+ _ -> True

13521384

13531385-- Try again to solve auto implicits

13541386solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

@@ -1376,14 +1408,26 @@ proofSearch' ist rec ambigok depth prv top n hints

13761408-- Resolve type classes. This will only pick up 'normal' instances, never

13771409-- named instances (hence using 'tcname' to check it's a generated instance

13781410-- name).

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1380−resolveTC = resTC' []

1381−

1382−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1383−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1384−resTC' tcs defaultOn depth topg fn ist

1385− = do compute

1386− g <- goal

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

1416+ -> IState -> ElabD ()

1417+resolveTC def mvok depth top fn ist

1418+ = do hs <- get_holes

1419+ resTC' [] def hs depth top fn ist

1420+

1421+resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1422+resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1423+resTC' tcs defaultOn topholes depth topg fn ist

1424+ = do compute

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

13871431 ptm <- get_term

13881432 ulog <- getUnifyLog

13891433 hs <- get_holes

@@ -1400,6 +1444,31 @@ resTC' tcs defaultOn depth topg fn ist

14001444 let depth' = if scopeOnly then 2 else depth

14011445 blunderbuss t depth' stk (stk ++ insts)) True

14021446 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+

14031472 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

14041473 | otherwise = (fail "Can't resolve", show n)

14051474

@@ -1427,10 +1496,13 @@ resTC' tcs defaultOn depth topg fn ist

14271496

14281497 blunderbuss t d stk [] = do -- c <- get_env

14291498 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1499+ lift $ tfail $ CantResolve False topg

14311500 blunderbuss t d stk (n:ns)

14321501 | n /= fn && (n `elem` stk || tcname n)

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1502+ = tryCatch (resolve n d)

1503+ (\e -> case e of

1504+ CantResolve True _ -> lift $ tfail e

1505+ _ -> blunderbuss t d stk ns)

14341506 | otherwise = blunderbuss t d stk ns

14351507

14361508 resolve n depth

@@ -1459,7 +1531,7 @@ resTC' tcs defaultOn depth topg fn ist

14591531 let got = fst (unApply t)

14601532 let depth' = if tc' `elem` tcs

14611533 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1534+ resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

14631535 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

14641536 -- if there's any arguments left, we've failed to resolve

14651537 hs <- get_holes

@@ -1505,11 +1577,17 @@ case_ ind autoSolve ist fn tm = do

15051577 else casetac (forget val)

15061578 when autoSolve solveAll

15071579

1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1580+tacN :: String -> Name

1581+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1582+

1583+runTactical :: FC -> Env -> Term -> ElabD ()

1584+runTactical fc env tm = do tm' <- eval tm

1585+ runTacTm tm'

1586+ return ()

15101587 where

1511− eval = normaliseAll ctxt env . finalise

1512− tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1588+ eval tm = do ctxt <- get_context

1589+ return $ normaliseAll ctxt env (finalise tm)

1590+

15131591 returnUnit = fmap fst $ get_type_val (Var unitCon)

15141592

15151593 -- | 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 ()

15471625 = do env <- get_env

15481626 fmap fst . get_type_val $ reflectEnv env

15491627 | n == tacN "prim__Fail", [_a, errs] <- args

1550− = do parts <- reifyReportParts (eval errs)

1628+ = do errs' <- eval errs

1629+ parts <- reifyReportParts errs'

15511630 lift . tfail $ ReflectionError [parts] (Msg "")

15521631 | n == tacN "prim__PureTactical", [_a, tm] <- args

15531632 = return tm

15541633 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1555− = do let first' = eval first

1634+ = do first' <- eval first

15561635 res <- runTacTm first'

1557− let next = eval (App andThen res)

1636+ next <- eval (App andThen res)

15581637 runTacTm next

15591638 | n == tacN "prim__Try", [_a, first, alt] <- args

1560− = do let first' = eval first

1561− let alt' = eval alt

1639+ = do first' <- eval first

1640+ alt' <- eval alt

15621641 try' (runTacTm first') (runTacTm alt') True

15631642 | n == tacN "prim__Fill", [raw] <- args

15641643 = do raw' <- reifyRaw raw

15651644 apply raw' []

15661645 returnUnit

1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

1568− = do n <- getNameFrom (sMN 0 hint)

1569− fmap fst $ get_type_val (reflectName n)

1646+ | n == tacN "prim__Gensym", [hint] <- args

1647+ = do hintStr <- eval hint

1648+ case hintStr of

1649+ Constant (Str h) -> do

1650+ n <- getNameFrom (sMN 0 h)

1651+ fmap fst $ get_type_val (reflectName n)

1652+ _ -> fail "no hint"

15701653 | n == tacN "prim__Claim", [n, ty] <- args

15711654 = do n' <- reifyTTName n

15721655 ty' <- reifyRaw ty

@@ -1596,6 +1679,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15961679 Just name -> fmap Just $ reifyTTName name

15971680 intro n

15981681 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

15991705 | n == tacN "prim__Debug", [ty, msg] <- args

16001706 = do let msg' = fromTTMaybe msg

16011707 case msg' of

@@ -1850,6 +1956,7 @@ runTac autoSolve ist perhapsFC fn tac

18501956 Just fc ->

18511957 do fill $ reflectFC fc

18521958 solve

1959+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

18531960 runT x = fail $ "Not implemented " ++ show x

18541961

18551962 runReflected t = do t' <- reify ist t

@@ -2361,7 +2468,7 @@ reflectTTQuote unq (P nt n t)

23612468reflectTTQuote unq (V n)

23622469 = reflCall "V" [RConstant (I n)]

23632470reflectTTQuote 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]

23652472reflectTTQuote unq (App f x)

23662473 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

23672474reflectTTQuote unq (Constant c)

@@ -2378,7 +2485,7 @@ reflectRawQuote unq (Var n)

23782485 | n `elem` unq = Var n

23792486 | otherwise = reflCall "Var" [reflectName n]

23802487reflectRawQuote 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]

23822489reflectRawQuote unq (RApp f x) =

23832490 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

23842491reflectRawQuote unq RType = Var (reflm "RType")

@@ -2436,27 +2543,27 @@ reflectNameQuotePattern _ -- for all other names, match any

24362543 solve

24372544

24382545reflectBinder :: Binder Term -> Raw

2439−reflectBinder = reflectBinderQuote reflectTTQuote []

2440−

2441−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2442−reflectBinderQuote q unq (Lam t)

2443− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2444−reflectBinderQuote q unq (Pi _ t k)

2445− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2446−reflectBinderQuote q unq (Let x y)

2447− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2448−reflectBinderQuote q unq (NLet x y)

2449− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2450−reflectBinderQuote q unq (Hole t)

2451− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2452−reflectBinderQuote q unq (GHole _ t)

2453− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2454−reflectBinderQuote q unq (Guess x y)

2455− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2456−reflectBinderQuote q unq (PVar t)

2457− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2458−reflectBinderQuote q unq (PVTy t)

2459− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2546+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2547+

2548+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2549+reflectBinderQuote q ty unq (Lam t)

2550+ = reflCall "Lam" [Var ty, q unq t]

2551+reflectBinderQuote q ty unq (Pi _ t k)

2552+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2553+reflectBinderQuote q ty unq (Let x y)

2554+ = reflCall "Let" [Var ty, q unq x, q unq y]

2555+reflectBinderQuote q ty unq (NLet x y)

2556+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2557+reflectBinderQuote q ty unq (Hole t)

2558+ = reflCall "Hole" [Var ty, q unq t]

2559+reflectBinderQuote q ty unq (GHole _ t)

2560+ = reflCall "GHole" [Var ty, q unq t]

2561+reflectBinderQuote q ty unq (Guess x y)

2562+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2563+reflectBinderQuote q ty unq (PVar t)

2564+ = reflCall "PVar" [Var ty, q unq t]

2565+reflectBinderQuote q ty unq (PVTy t)

2566+ = reflCall "PVTy" [Var ty, q unq t]

24602567

24612568mkList :: Raw -> [Raw] -> Raw

24622569mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2603,11 +2710,15 @@ reflectErr (NotInjective t1 t2 t3) =

26032710 , reflect t2

26042711 , reflect t3

26052712 ]

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]

26072715reflectErr (CantResolveAlts ss) =

26082716 raw_apply (Var $ reflErrName "CantResolveAlts")

26092717 [rawList (Var $ reflm "TTName") (map reflectName ss)]

26102718reflectErr (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]

26112722reflectErr UniverseError = Var $ reflErrName "UniverseError"

26122723reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

26132724reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2748,6 +2859,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

27482859 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

27492860reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

27502861

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+

27512884envTupleType :: Raw

27522885envTupleType

27532886 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/IBC.hs+12−8

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

@@ -365,7 +365,7 @@ pClasses cs = mapM_ (\ (n, c) ->

365365 -- Don't lose instances from previous IBCs, which

366366 -- could have loaded in any order

367367 let is = case lookupCtxtExact n (idris_classes i) of

368− Just (CI _ _ _ _ _ ins) -> ins

368+ Just (CI _ _ _ _ _ ins _) -> ins

369369 _ -> []

370370 let c' = c { class_instances =

371371 class_instances c ++ is }

@@ -1241,7 +1241,7 @@ instance (Binary t) => Binary (PDecl' t) where

12411241 put x10

12421242 put x11

12431243 put x12

1244− PClass x1 x2 x3 x4 x5 x6 x7 x8

1244+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

12451245 -> do putWord8 7

12461246 put x1

12471247 put x2

@@ -1251,6 +1251,7 @@ instance (Binary t) => Binary (PDecl' t) where

12511251 put x6

12521252 put x7

12531253 put x8

1254+ put x9

12541255 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

12551256 do putWord8 8

12561257 put x1

@@ -1352,7 +1353,8 @@ instance (Binary t) => Binary (PDecl' t) where

13521353 x6 <- get

13531354 x7 <- get

13541355 x8 <- get

1355− return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1356+ x9 <- get

1357+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

13561358 8 -> do x1 <- get

13571359 x2 <- get

13581360 x3 <- get

@@ -1424,7 +1426,7 @@ instance Binary Using where

14241426 _ -> error "Corrupted binary data for Using"

14251427

14261428instance Binary SyntaxInfo where

1427− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1429+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

14281430 = do put x1

14291431 put x2

14301432 put x3

@@ -1440,7 +1442,7 @@ instance Binary SyntaxInfo where

14401442 x5 <- get

14411443 x6 <- get

14421444 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)

14441446

14451447instance (Binary t) => Binary (PClause' t) where

14461448 put x

@@ -2077,19 +2079,21 @@ instance (Binary t) => Binary (PArg' t) where

20772079

20782080

20792081instance Binary ClassInfo where

2080− put (CI x1 x2 x3 x4 x5 _)

2082+ put (CI x1 x2 x3 x4 x5 _ x6)

20812083 = do put x1

20822084 put x2

20832085 put x3

20842086 put x4

20852087 put x5

2088+ put x6

20862089 get

20872090 = do x1 <- get

20882091 x2 <- get

20892092 x3 <- get

20902093 x4 <- get

20912094 x5 <- get

2092− return (CI x1 x2 x3 x4 x5 [])

2095+ x6 <- get

2096+ return (CI x1 x2 x3 x4 x5 [] x6)

20932097

20942098instance Binary OptInfo where

20952099 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

@@ -585,8 +585,8 @@ collect (c@(PClauses _ o _ _) : ds)

585585collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

586586collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588−collect (PClass doc f s cs n ps pdocs ds : ds')

589− = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

588+collect (PClass doc f s cs n ps pdocs fds ds : ds')

589+ = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

590590collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591591 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592592collect (d : ds) = d : collect ds

src/Idris/Parser.hs+5−1

@@ -612,11 +612,15 @@ class_ syn = do (doc, argDocs, acc)

612612 n_in <- fnName

613613 let n = expandNS syn n_in

614614 cs <- many carg

615+ fds <- option (map fst cs) fundeps

615616 ds <- option [] (classBlock syn)

616617 accData acc n (concatMap declared ds)

617− return [PClass doc syn fc cons n cs argDocs ds]

618+ return [PClass doc syn fc cons n cs argDocs fds ds]

618619 <?> "type-class declaration"

619620 where

621+ fundeps :: IdrisParser [Name]

622+ fundeps = do lchar '|'; sepBy name (lchar ',')

623+

620624 carg :: IdrisParser (Name, PTerm)

621625 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

622626 return (i, ty)

src/Idris/Prover.hs+1−1

@@ -78,7 +78,7 @@ prove opt ctxt lit n ty

7878 putIState (i { proof_list = (n, prf) : proofs })

7979 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

8080 logLvl 3 (show tree)

81− (ptm, pty) <- recheckC (fileFC "proof") [] tm

81+ (ptm, pty) <- recheckC (fileFC "proof") id [] tm

8282 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

8383 "Expected type:" ++ show ty)

8484 case converts ctxt [] ty pty of

src/Idris/REPL.hs+1−1

@@ -773,7 +773,7 @@ process fn (NewDefn decls) = do

773773 getName (PTy docs argdocs syn fc opts name ty) = Just name

774774 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

775775 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

776− getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name

776+ getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

777777 getName _ = Nothing

778778 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

779779 getClauseName (PClause fc name whole with rhs whereBlock) = name

src/Idris/Reflection.hsnew file+18

@@ -0,0 +1,18 @@

1+{-|

2+Handy tools for doing reflection.

3+-}

4+module Idris.Reflection where

5+

6+import Idris.Core.TT

7+import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))

8+

9+data RArg = RExplicit { argName :: Name, argTy :: Raw }

10+ | RImplicit { argName :: Name, argTy :: Raw }

11+ | RConstraint { argName :: Name, argTy :: Raw }

12+

13+data RTyDecl = RDeclare Name [RArg] Raw

14+

15+rArgToPArg :: RArg -> PArg

16+rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

17+rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

18+rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

src/Idris/TypeSearch.hs+1−1

@@ -46,7 +46,7 @@ searchByType pkgs pterm = do

4646 mapM_ loadPkgIndex pkgs

4747 pterm' <- addUsingConstraints syn emptyFC pterm

4848 pterm'' <- implicit toplevel syn name pterm'

49− let pterm''' = addImpl i pterm''

49+ let pterm''' = addImpl [] i pterm''

5050 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

5151 let names = searchUsing searchPred i ty

5252 let names' = take numLimit names

test/basic002/test006.idr+1−1

@@ -18,7 +18,7 @@ natToBin k with (parity k)

1818 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

1919

2020main : IO ()

21−main = do print (natToBin 42)

21+main = do printLn (natToBin 42)

2222

2323---------- Proofs ----------

2424

test/basic003/test027.idr+3−3

@@ -19,7 +19,7 @@ using (Ord a, Num n)

1919 mprod (x :: xs) = x * mprod xs

2020

2121main : IO ()

22−main = do print $ isort [1,5,3,5,1,9,8]

23− print $ msum [1..10]

24− print $ mprod [1..10]

22+main = do printLn $ isort [1,5,3,5,1,9,8]

23+ printLn $ msum [1..10]

24+ printLn $ mprod [1..10]

2525

test/basic004/test016.idr+1−1

@@ -13,5 +13,5 @@ take (S n) (x :: xs) = x :: take n xs

1313take n [] = []

1414

1515main : IO ()

16−main = do print (take 10 (Main.countFrom 10))

16+main = do printLn (take 10 (Main.countFrom 10))

1717

test/basic005/test019.lidr+1−1

@@ -14,5 +14,5 @@

1414> | False = ifFalse x

1515

1616> main : IO ()

17−> main = print (test ((S 4) ==) 5 Oh)

17+> main = printLn (test ((S 4) ==) 5 Oh)

1818

test/basic006/test020.idr+2−2

@@ -21,7 +21,7 @@ test : Integer -> String

2121test x = "Number " ++ x

2222

2323main : IO ()

24−main = do print (foo [1,2,3])

25− print (test 42)

24+main = do printLn (foo [1,2,3])

25+ printLn (test 42)

2626

2727

test/basic006/test020a.idr+1−1

@@ -16,5 +16,5 @@ foo : Vect n a -> List a

1616foo xs = reverse xs

1717

1818main : IO ()

19−main = print (foo [1,2,3])

19+main = printLn (foo [1,2,3])

2020

test/basic007/test033.idr+1−1

@@ -1,4 +1,4 @@

11module Main

22

33main : IO ()

4−main = nullPtr null >>= print

4+main = nullPtr null >>= printLn

test/basic011/basic011.idr+10−10

@@ -3,14 +3,14 @@ module Main

33import Data.Hash

44

55main : IO ()

6−main = do print $ hash (the Bits8 3)

7− print $ hash (the (List Bits8) [3])

8− print $ hash "hello world"

9− print $ hash 'a'

10− print $ hash (the Bits8 3)

11− print $ hash (the Bits16 3)

12− print $ hash (the Bits32 3)

13− print $ hash (the Bits64 3)

14− print $ hash (the Int 3)

15− print $ hash (the Integer 3)

6+main = do printLn $ hash (the Bits8 3)

7+ printLn $ hash (the (List Bits8) [3])

8+ printLn $ hash "hello world"

9+ printLn $ hash 'a'

10+ printLn $ hash (the Bits8 3)

11+ printLn $ hash (the Bits16 3)

12+ printLn $ hash (the Bits32 3)

13+ printLn $ hash (the Bits64 3)

14+ printLn $ hash (the Int 3)

15+ printLn $ hash (the Integer 3)

1616

test/basic012/basic012.idr+5−4

@@ -1,7 +1,7 @@

11import Data.Vect

22import Control.Monad.State

33import Control.Monad.Identity

4−

4+

55VThing : Type

66VThing = {n : Nat} -> Vect n Int -> Int

77

@@ -31,7 +31,8 @@ testfoo3 xs = foo 42 xs (bar 10)

3131AnyST : Type -> Type -> Type

3232AnyST s a = {m : _} -> Monad m => StateT s m a

3333

34−foost: AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

3536foost = do x <- get

3637 put x

3738

@@ -52,11 +53,11 @@ tupleId f (a, b) = (f a, f b)

5253

5354AppendType : Type

5455AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55−

56+

5657append : AppendType

5758append [] ys = ys

5859append (x :: xs) ys = x :: append xs ys

5960

6061main : IO ()

6162main = do putStrLn (baz 42)

62− print (append [1,2,3] [4,5,6])

63+ printLn (append [1,2,3] [4,5,6])

test/dsl001/test001.idr+2−2

@@ -96,8 +96,8 @@ testEnv : Int -> Env [TyInt,TyInt]

9696testEnv x = [x,x]

9797

9898main : IO ()

99−main = do { print testFac

100− print test }

99+main = do { printLn testFac

100+ printLn test }

101101

102102

103103

test/effects002/test025.idr+1−1

@@ -30,6 +30,6 @@ testMemory = do Src :- allocate 5

3030

3131main : IO ()

3232main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

33− (\err => print err) (\ok => print ok)

33+ (\err => printLn err) (\ok => printLn ok)

3434

3535

test/io002/test008.idr+1−1

@@ -22,7 +22,7 @@ main = do (a, b) <- ioVals

2222 let x = "bar"

2323 putStrLn (show (getVal x 7 testlist))

2424 let ((y, z) :: _) = testlist

25− print z

25+ printLn z

2626 case lookup x testlist of

2727 Just v => putStrLn (show v)

2828 Nothing => putStrLn "Not there!"

test/io003/test018a.idr+1−1

@@ -27,7 +27,7 @@ mainProc = do mainID <- myID

2727

2828repeatIO : Int -> IO ()

2929repeatIO 0 = return ()

30−repeatIO n = do print n

30+repeatIO n = do printLn n

3131 run mainProc

3232 repeatIO (n - 1)

3333

test/primitives001/test005.idr+6−6

@@ -7,9 +7,9 @@ tlist : List Int

77tlist = [1, 2, 3, 4, 5]

88

99main : IO ()

10−main = do print (abs (-8))

11− print (abs (S Z))

12− print (span isAlpha tstr)

13− print (break isDigit tstr)

14− print (span (\x => x < 3) tlist)

15− print (break (\x => x > 2) tlist)

10+main = do printLn (abs (-8))

11+ printLn (abs (S Z))

12+ printLn (span isAlpha tstr)

13+ printLn (break isDigit tstr)

14+ printLn (span (\x => x < 3) tlist)

15+ printLn (break (\x => x > 2) tlist)

test/proof003/test015.idr+3−3

@@ -72,10 +72,10 @@ readNum = do putStr "Enter a number:"

7272

7373main : IO ()

7474main = do let Just bin1 = natToBin 8 42

75− print bin1

75+ printLn bin1

7676 let Just bin2 = natToBin 8 89

77− print bin2

78− print (adc bin1 bin2 b0)

77+ printLn bin2

78+ printLn (adc bin1 bin2 b0)

7979

8080

8181

test/quasiquote001/expected+2−2

@@ -1,5 +1,5 @@

11(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))))))

22--------------

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)))))

44--------------

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

2222main : IO ()

2323main = do let x = record { name = "foo",

2424 more_things = reverse ["a","b"] } testFoo

25− print $ name x

26− print $ name person

27− print $ things x

28− print $ more_things x

29− print $ age (record { age = 25 } person)

25+ printLn $ name x

26+ printLn $ name person

27+ printLn $ things x

28+ printLn $ more_things x

29+ printLn $ age (record { age = 25 } person)

3030

test/records003/records003.idr+6−13

@@ -1,9 +1,6 @@

11record Person (age : Nat) where

22 constructor MkPerson

33 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

74

85record Event where

96 constructor MkEvent

@@ -18,9 +15,6 @@ record Meeting (year : Int) where

1815new_organiser : String -> List (Meeting x) -> List (Meeting x)

1916new_organiser n = map (record { event->organiser->name = n })

2017

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−

2418next_year : Meeting x -> Meeting (x+1)

2519next_year m = record { organiser->param_age

2620 = record { organiser->param_age } m + 1,

@@ -44,10 +38,9 @@ test : Meeting 2015

4438test = next_year idm_gbg

4539

4640main : IO ()

47−main = do print (record { event->organiser->name } test)

48− print (record { event->organiser->param_age } test)

49− print (record { event->organiser->param_age } idm_gbg)

50− print (record { organiser->param_age } test)

51− print (record { organiser->param_age } idm_gbg)

52− print (record { param_year } idm_gbg)

53−

41+main = do printLn (record { event->organiser->name } test)

42+ printLn (record { event->organiser->param_age } test)

43+ printLn (record { event->organiser->param_age } idm_gbg)

44+ printLn (record { organiser->param_age } test)

45+ printLn (record { organiser->param_age } idm_gbg)

46+ printLn (record { param_year } idm_gbg)

test/reg002/reg012.idr+1−1

@@ -30,4 +30,4 @@ swap (x :: Nil) = x :: Nil

3030swap (x :: y :: xs) = (y :: x :: (swap xs))

3131

3232main : IO ()

33−main = print (swap [1,2,3,4,5])

33+main = printLn (swap [1,2,3,4,5])

test/reg004/reg004.idr+1−1

@@ -13,4 +13,4 @@ h True = r2 where

1313 r2 = r

1414

1515main : IO ()

16−main = do print (h True); print (h False)

16+main = do printLn (h True); printLn (h False)

test/reg013/reg013.idr+3−3

@@ -2,7 +2,7 @@ module Main

22

33main : IO ()

44main = do

5− print $ prim_lenString "hallo"

6− print $ prim_lenString "1"

7− print $ prim_lenString ""

5+ printLn $ prim_lenString "hallo"

6+ printLn $ prim_lenString "1"

7+ printLn $ prim_lenString ""

88

test/reg016/reg016.idr+6−6

@@ -1,11 +1,11 @@

11module Main

22

33main : IO ()

4−main = do print $ the Integer 429496729500000000000000

5−-- print $ the Integer 4294967296

6−-- print $ the Integer 4294967297

7−-- print $ the Int 4294967295

8−-- print $ the Int 4294967296

9−-- print $ the Int 4294967297

4+main = do printLn $ the Integer 429496729500000000000000

5+-- printLn $ the Integer 4294967296

6+-- printLn $ the Integer 4294967297

7+-- printLn $ the Int 4294967295

8+-- printLn $ the Int 4294967296

9+-- printLn $ the Int 4294967297

1010

1111

test/reg017/reg017.idr+1−1

@@ -10,4 +10,4 @@ foo : { t : Type } ->

1010foo {t} a {prfA = p} b c {prfBC} = b

1111

1212main : IO ()

13−main = print $ foo 3 4 4

13+main = printLn $ foo 3 4 4

test/reg018/reg018d.idr+1−1

@@ -12,4 +12,4 @@ pull {n=S _} (FS n) (x :: xs) =

1212 (v, x::vs)

1313

1414main : IO ()

15−main = print (pull FZ [0, 1, 2])

15+main = printLn (pull FZ [0, 1, 2])

test/reg027/reg027.idr+1−1

@@ -27,6 +27,6 @@ foo = do val <- dbl

2727 \x => show val

2828

2929main : IO ()

30−main = do print dbl

30+main = do printLn dbl

3131 putStrLn (foo 3)

3232

test/reg029/reg029.idr+2−2

@@ -7,5 +7,5 @@ import System

77

88main : IO ()

99main = do

10− print !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11− print !(getEnv "IDRIS_REG029_EXISTENT_VAR")

10+ printLn !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11+ printLn !(getEnv "IDRIS_REG029_EXISTENT_VAR")

test/reg031/reg031.idr+1−1

@@ -1,7 +1,7 @@

11module Main

22

33main : IO ()

4−main = print . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

4+main = printLn . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

55 where

66 -- make the values positive if the backend has signed chars

77 val : Char -> Int

test/reg040/reg040.idr+1−1

@@ -4,4 +4,4 @@ io : IO Int

44io = return 42

55

66main : IO ()

7−main = print $ unsafePerformIO io

7+main = printLn $ unsafePerformIO io

test/reg042/reg042.idr+1−1

@@ -21,4 +21,4 @@ g (C x y z) = x + y

2121-- Here, we'd apply the not-a-function to the erased argument 4,

2222-- which would make the program go wrong.

2323main : IO ()

24−main = print $ g (proj 3 f 4)

24+main = printLn $ g (proj 3 f 4)

test/reg045/reg045.idr+1−1

@@ -15,5 +15,5 @@ foo : ListZ Nat

1515foo = (1 :: 2 :: 3 :: Nil)

1616

1717main : IO ()

18−main = print foo

18+main = printLn foo

1919

test/reg052/reg052.idr+1−1

@@ -5,4 +5,4 @@ impure_int : IO Int

55impure_int = return 41

66

77main : IO ()

8−main = impure_int >>= impure_op . prim__zextInt_B64 >>= print

8+main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/reg059/expectednew file

No changes to the content.

test/reg059/reg059.idrnew file+8

@@ -0,0 +1,8 @@

1+class Monad m => ContainerMonad (m : Type -> Type) where

2+ Elem : a -> m a -> Type

3+ tagElem : (mx : m a) -> m (x : a ** Elem x mx)

4+

5+class Monad m => ContainerMonad2 a (m : Type -> Type) where

6+ Elem2 : a -> m a -> Type

7+ tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

8+

test/reg059/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg059.idr --check

3+rm -f *.ibc

test/sourceLocation001/SourceLoc.idr+4−4

@@ -36,7 +36,7 @@ using (ctxt : Vect n Ty)

3636 Var : (i : Fin n) -> Tm ctxt (index i ctxt)

3737 Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

3838 App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'

39− ||| A term that makes the program halt and print where it halted

39+ ||| A term that makes the program halt and printLn where it halted

4040 Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

4141

4242 data Env : Vect n Ty -> Type where

@@ -83,11 +83,11 @@ testTerm4 = App testTerm3 MkU

8383namespace Main

8484 main : IO ()

8585 main = do putStrLn "Testing using definition"

86− print fromRHS

86+ printLn fromRHS

8787 putStrLn "Testing using inline tactics"

88− print fromProofScript

88+ printLn fromProofScript

8989 putStrLn "Testing using metavariable with later definition"

90− print fromMetavar

90+ printLn fromMetavar

9191 putStrLn "-----------------------"

9292 sequence_ $ with List [ exec testTerm1

9393 , exec testTerm2

test/sugar001/test007.idr+4−4

@@ -35,7 +35,7 @@ runEval env e with (eval e) {

3535}

3636

3737main : IO ()

38−main = do print [| (\x => x *2) (Just 4) |]

39− print [| plus (Just 4) (Just 5) |]

40− print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41− print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

38+main = do printLn [| (\x => x *2) (Just 4) |]

39+ printLn [| plus (Just 4) (Just 5) |]

40+ printLn (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41+ printLn (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

test/sugar004/sugar004.idr+1−1

@@ -9,7 +9,7 @@ foo x = let Just x' = x | Nothing => 100 in x'

99main : IO ()

1010main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

1111 | (x :: y :: _) => putStrLn "Too many arguments!"

12− print (foo (Just (cast a)))

12+ printLn (foo (Just (cast a)))

1313

1414{-

1515

test/sugar005/As.idr+9−9

@@ -24,13 +24,13 @@ same _ _ = Nothing

2424

2525namespace Main

2626 main : IO ()

27− main = do print $ isS 0

28− print $ isS 1

29− print $ hasS [0,0,0]

30− print $ hasS [0,1,2]

31− print $ isSS 5

32− print $ isSS 0

33− print $ same 1 1

34− print $ same 0 0

35− print $ same 1 0

27+ main = do printLn $ isS 0

28+ printLn $ isS 1

29+ printLn $ hasS [0,0,0]

30+ printLn $ hasS [0,1,2]

31+ printLn $ isSS 5

32+ printLn $ isSS 0

33+ printLn $ same 1 1

34+ printLn $ same 0 0

35+ printLn $ same 1 0

3636

test/tactics001/Tactics.idr+14

@@ -2,6 +2,9 @@ module Tactics

22

33import Language.Reflection.Tactical

44

5+import Data.Vect

6+

7+

58%default total

69

710-- Test that basic proofs with new-style tactics work

@@ -25,3 +28,14 @@ plusSuccRightSuccNew (S j) k =

2528 %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

2629 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

2730 solve)

31+

32+-- Test that side effects in new tactics work

33+

34+mkDecl : ()

35+mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

36+ [Implicit (UN "z") `(Nat)]

37+ `(Vect ~(Var (UN "z")) ())

38+ fill `(() : ())

39+ solve)

40+

41+repUnit = pure ()

test/totality004/totality004.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

2121countStream x = x :: countStream (x + 1)

2222

2323main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

2525

test/totality004/totality004a.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

2121countStream x = x :: countStream (x + 1)

2222

2323main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

2525

test/totality005/totality005.idr+1−1

@@ -7,4 +7,4 @@ fib : Stream Nat

77fib = 0 :: zipWithS (+) fib (1 :: fib)

88

99partial main : IO ()

10−main = print (take 15 fib)

10+main = printLn (take 15 fib)

test/tutorial002/tutorial002.idr+1−1

@@ -34,7 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

3434main : IO ()

3535main = do putStr "Enter a number: "

3636 x <- getLine

37− print (natToBin (fromInteger (cast x)))

37+ printLn (natToBin (fromInteger (cast x)))

3838

3939---------- Proofs ----------

4040

test/unique001/expected+1−1

@@ -17,4 +17,4 @@ with

1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS

1818unique001c.idr:46:6:Unique name f is used more than once

1919unique001d.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