a713659 · Idris-dev · git.iko.soy

.travis.yml+8−6

@@ -6,6 +6,8 @@ before_install:

6 - sudo apt-get install -qq libghc-unordered-containers-dev libghc-mtl-dev libghc-network-dev libghc-xml-dev libghc-transformers-dev libghc-text-dev libghc-utf8-string-dev libghc-vector-dev libghc-split-dev libghc-ansi-terminal-dev libghc-ansi-wl-pprint-dev

7 # trifecta dependencies

8 - sudo apt-get install -qq libghc-blaze-builder-dev libghc-blaze-html-dev libghc-data-lens-dev libghc-bifunctors-dev libghc-hashable-dev libghc-semigroups-dev libghc-semigroupoids-dev libghc-parallel-dev libghc-comonad-dev libghc-terminfo-dev libghc-keys-dev

9+ # Haddock dependencies

10+ - sudo apt-get install hscolour

9 # test dependency

11 # test dependency

10 - sudo apt-get install -qq expect

12 - sudo apt-get install -qq expect

11install:

13install:

@@ -17,11 +19,11 @@ before_script:

17 - cd idris*

19 - cd idris*

18script:

20script:

19 - cabal configure -f FFI -f LLVM

21 - cabal configure -f FFI -f LLVM

20− - cabal build

22+ - if [[ "$TESTS" != "doc" ]]; then cabal build; fi

21− - cabal copy

23+ - if [[ "$TESTS" != "doc" ]]; then cabal copy; fi

22 - make -j2 $TESTS

24 - make -j2 $TESTS

23env:

25env:

24− # TESTS=doc

26+ - TESTS="doc"

25− - TESTS=test_c

27+ - TESTS="test_c"

26− - TESTS=test_llvm

28+ - TESTS="test_llvm"

27− - TESTS=test_js

29+ - TESTS="test_js"

CHANGELOG+7

@@ -6,6 +6,7 @@ New in 0.9.13:

6* Command line option -e (or --eval) to evaluate expressions without loading the

7 REPL. This is useful for writing more portable tests.

8* Many more of the basic functions and datatypes are documented.

9+* Primitive types such as Int and String are documented

9* Removed javascript lib in favor of idris-hackers/iQuery

10* Removed javascript lib in favor of idris-hackers/iQuery

10* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)

11* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)

11* Remove :info REPL command, subsume and enhance its functionality in the :doc command

12* Remove :info REPL command, subsume and enhance its functionality in the :doc command

@@ -13,6 +14,12 @@ New in 0.9.13:

13 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val

14 record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val

14 record { a->b->c } x -- accesses field, equivalent to c (b (a x))

15 record { a->b->c } x -- accesses field, equivalent to c (b (a x))

15* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.

16* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.

17+* :apropos now accepts space-delimited lists of query items, and searches for the conjunction

18+ of its inputs. It also accepts binder syntax as search strings - for instance, -> finds

19+ functions.

20+* Totality errors are now treated as warnings until code generation time, when they become

21+ errors again. This allows users to use the interactive editing features to fix totality

22+ issues, but no programs that violate the stated assumptions will actually run.

16

23

17Internal changes

24Internal changes

18

25

Makefile+1−1

@@ -43,7 +43,7 @@ linecount:

43

44#Note: this doesn't yet link to Hackage properly

45doc: dist/setup-config

46− $(CABAL) haddock --executables --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

46+ $(CABAL) haddock --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

47

48

49dist/setup-config:

idris.cabal+8−1

@@ -235,6 +235,8 @@ Extra-source-files:

235 test/reg042/run

236 test/reg042/*.idr

237 test/reg042/expected

238+ test/reg043/run

239+ test/reg043/expected

238

240

239 test/basic001/run

241 test/basic001/run

240 test/basic001/*.idr

242 test/basic001/*.idr

@@ -442,6 +444,10 @@ Extra-source-files:

442 test/totality006/run

444 test/totality006/run

443 test/totality006/*.idr

445 test/totality006/*.idr

444 test/totality006/expected

446 test/totality006/expected

447+ test/totality007/run

448+ test/totality007/*.ipkg

449+ test/totality007/src/*.idr

450+ test/totality007/expected

445

451

446 test/tutorial001/run

452 test/tutorial001/run

447 test/tutorial001/*.idr

453 test/tutorial001/*.idr

@@ -534,6 +540,7 @@ Library

534 , Idris.IdrisDoc

540 , Idris.IdrisDoc

535 , Idris.Imports

541 , Idris.Imports

536 , Idris.Inliner

542 , Idris.Inliner

543+ , Idris.Interactive

537 , Idris.Output

544 , Idris.Output

538 , Idris.Parser

545 , Idris.Parser

539 , Idris.ParseHelpers

546 , Idris.ParseHelpers

@@ -592,7 +599,7 @@ Library

592 , ansi-wl-pprint

599 , ansi-wl-pprint

593 , binary

600 , binary

594 , blaze-html >= 0.6.1.3

601 , blaze-html >= 0.6.1.3

595− , blaze-markup >= 0.5.2.1 && < 0.6.0.0

602+ , blaze-markup >= 0.5.2.1 && < 0.7.0.0

596 , bytestring

603 , bytestring

597 , cheapskate

604 , cheapskate

598 , containers >= 0.5

605 , containers >= 0.5

libs/base/Data/List.idrnew file+30

@@ -0,0 +1,30 @@

1+module Data.List

2+

3+%access public

4+

5+using (xs : List a)

6+ ||| A proof that some element is found in a list

7+ data Elem : a -> List a -> Type where

8+ Here : Elem x (x :: xs)

9+ There : Elem x xs -> Elem x (y :: xs)

10+

11+ instance Uninhabited (Elem {a} x []) where

12+ uninhabited Here impossible

13+ uninhabited (There p) impossible

14+

15+ isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

16+ isElem x [] = No absurd

17+ isElem x (y :: xs) with (decEq x y)

18+ isElem x (x :: xs) | (Yes refl) = Yes Here

19+ isElem x (y :: xs) | (No contra) with (isElem x xs)

20+ isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)

21+ isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

22+ where

23+ mkNo : {xs' : List a} ->

24+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

25+ Elem x' (y' :: xs') -> _|_

26+ mkNo f g Here = f refl

27+ mkNo f g (There x) = g x

28+

29+

30+

libs/base/base.ipkg+1

@@ -23,6 +23,7 @@ modules = System,

23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

24 Data.Floats, Data.Complex, Data.Heap, Data.Fun,

25 Data.Rel, Data.Buffer, Data.Erased,

26+ Data.List,

26

27

27 Control.Isomorphism, Control.Isomorphism.Primitives,

28 Control.Isomorphism, Control.Isomorphism.Primitives,

28 Control.Monad.Identity,

29 Control.Monad.Identity,

libs/effects/Effects.idr+2−2

@@ -337,8 +337,8 @@ mapVE f [] = pure []

337mapVE f (x :: xs) = [| f x :: mapVE f xs |]

338

339

340−when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()

340+when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()

341−when True e = e

341+when True e = Force e

342when False e = pure ()

343

344-- --------------------------------------------------------------------- [ EOF ]

libs/oldeffects/Effects.idr+1−1

@@ -303,6 +303,6 @@ mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)

303mapE f [] = pure []

304mapE f (x :: xs) = [| f x :: mapE f xs |]

305

306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

306+when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()

307when True e = e

308when False e = pure ()

libs/prelude/Prelude/Applicative.idr+5−2

@@ -38,8 +38,11 @@ class Applicative f => Alternative (f : Type -> Type) where

38 empty : f a

39 (<|>) : f a -> f a -> f a

40

41+||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`

41guard : Alternative f => Bool -> f ()

42guard : Alternative f => Bool -> f ()

42guard a = if a then pure () else empty

43guard a = if a then pure () else empty

43

44

45+||| Conditionally execute an applicative expression

44−when : Applicative f => Bool -> f () -> f ()

46+when : Applicative f => Bool -> Lazy (f ()) -> f ()

45−when a f = if a then f else pure ()

47+when True f = Force f

48+when False f = pure ()

libs/prelude/Prelude/Bool.idr+13−5

@@ -15,7 +15,15 @@ boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

15boolElim True t e = t

16boolElim False t e = e

17

18−||| Defines a predicate on Bool which guarantees that the value is true.

18+||| Ensure that some run-time Boolean test has been performed.

19+|||

20+||| This lifts a Boolean predicate to the type level. See the function `choose`

21+||| if you need to perform a Boolean test and convince the type checker of this

22+||| fact.

23+|||

24+||| If you find yourself using `so` for something other than primitive types,

25+||| it may be appropriate to define a type of evidence for the property that you

26+||| care about instead.

19data so : Bool -> Type where oh : so True

27data so : Bool -> Type where oh : so True

20

28

21instance Uninhabited (so False) where

29instance Uninhabited (so False) where

@@ -27,13 +35,13 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

27-- Boolean Operator Precedence

35-- Boolean Operator Precedence

28infixl 4 &&, ||

36infixl 4 &&, ||

29

37

30−||| Boolean OR

38+||| Boolean OR only evaluates the second argument if the first is `False`.

31−(||) : Bool -> Bool -> Bool

39+(||) : Bool -> Lazy Bool -> Bool

32(||) False x = x

40(||) False x = x

33(||) True _ = True

41(||) True _ = True

34

42

35−||| Boolean AND

43+||| Boolean AND only evaluates the second argument if the first is `True`.

36−(&&) : Bool -> Bool -> Bool

44+(&&) : Bool -> Lazy Bool -> Bool

37(&&) True x = x

45(&&) True x = x

38(&&) False _ = False

46(&&) False _ = False

39

47

libs/prelude/Prelude/Either.idr+4−4

@@ -39,9 +39,9 @@ choose False = Right oh

39||| @ f the action to take on Left

40||| @ g the action to take on Right

41||| @ e the sum to analyze

42−either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c

42+either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c

43−either l r (Left x) = l x

43+either l r (Left x) = (Force l) x

44−either l r (Right x) = r x

44+either l r (Right x) = (Force r) x

45

46||| Keep the payloads of all Left constructors in a list of Eithers

47lefts : List (Either a b) -> List a

@@ -74,7 +74,7 @@ fromEither (Right r) = r

74

75||| Convert a Maybe to an Either by using a default value in case of Nothing

76||| @ e the default value

77−maybeToEither : (def : e) -> Maybe a -> Either e a

77+maybeToEither : (def : Lazy e) -> Maybe a -> Either e a

78maybeToEither def (Just j) = Right j

79maybeToEither def Nothing = Left def

80

libs/prelude/Prelude/Foldable.idr+25−8

@@ -14,27 +14,44 @@ class Foldable (t : Type -> Type) where

14foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc

15foldl f z t = foldr (flip (.) . flip f) id t z

16

17+||| Combine each element of a structure into a monoid

17concat : (Foldable t, Monoid a) => t a -> a

18concat : (Foldable t, Monoid a) => t a -> a

18concat = foldr (<+>) neutral

19concat = foldr (<+>) neutral

19

20

21+||| Combine into a monoid the collective results of applying a function

22+||| to each element of a structure

20concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m

23concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m

21concatMap f = foldr ((<+>) . f) neutral

24concatMap f = foldr ((<+>) . f) neutral

22

25

26+||| The conjunction of all elements of a structure containing

27+||| lazy boolean values. `and` short-circuits from left to right,

28+||| evaluating until either an element is `False` or no elements remain.

23−and : Foldable t => t Bool -> Bool

29+and : Foldable t => t (Lazy Bool) -> Bool

24−and = foldr (&&) True

30+and = foldl (&&) True

25−

31+

32+||| The disjunction of all elements of a structure containing

33+||| lazy boolean values. `or` short-circuits from left to right, evaluating

34+||| either until an element is `True` or no elements remain.

26−or : Foldable t => t Bool -> Bool

35+or : Foldable t => t (Lazy Bool) -> Bool

27−or = foldr (||) False

36+or = foldl (||) False

28−

37+

38+||| The disjunction of the collective results of applying a

39+||| predicate to all elements of a structure. `any` short-circuits

40+||| from left to right.

29any : Foldable t => (a -> Bool) -> t a -> Bool

41any : Foldable t => (a -> Bool) -> t a -> Bool

30−any p = foldr ((||) . p) False

42+any p = foldl (\x => \y => x || p y) False

31

43

44+||| The disjunction of the collective results of applying a

45+||| predicate to all elements of a structure. `all` short-circuits

46+||| from left to right.

32all : Foldable t => (a -> Bool) -> t a -> Bool

47all : Foldable t => (a -> Bool) -> t a -> Bool

33−all p = foldr ((&&) . p) True

48+all p = foldl (\x => \y => x && p y) True

34

49

50+||| Add together all the elements of a structure

35sum : (Foldable t, Num a) => t a -> a

51sum : (Foldable t, Num a) => t a -> a

36sum = foldr (+) 0

52sum = foldr (+) 0

37

53

54+||| Multiply together all elements of a structure

38product : (Foldable t, Num a) => t a -> a

55product : (Foldable t, Num a) => t a -> a

39product = foldr (*) 1

56product = foldr (*) 1

40

57

libs/prelude/Prelude/List.idr+2−2

@@ -182,9 +182,9 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

182||| @ nil what to return at the end of the list

183||| @ cons what to do at each step of recursion

184||| @ xs the list to recurse over

185−list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a

185+list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b

186list nil cons [] = nil

187−list nil cons (x::xs) = cons x xs

187+list nil cons (x::xs) = (Force cons) x xs

188

189--------------------------------------------------------------------------------

190-- Building (bigger) lists

libs/prelude/Prelude/Maybe.idr+10−3

@@ -28,25 +28,32 @@ isJust (Just j) = True

28-- Misc

29--------------------------------------------------------------------------------

30

31−maybe : Lazy b -> (a -> b) -> Maybe a -> b

31+maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

32maybe n j Nothing = n

33−maybe n j (Just x) = j x

33+maybe n j (Just x) = (Force j) x

34

35+||| Convert a `Maybe a` value to an `a` value by providing a default `a` value

36+||| in the case that the `Maybe` value is `Nothing`.

35fromMaybe : (Lazy a) -> Maybe a -> a

37fromMaybe : (Lazy a) -> Maybe a -> a

36fromMaybe def Nothing = def

38fromMaybe def Nothing = def

37fromMaybe def (Just j) = j

39fromMaybe def (Just j) = j

38

40

41+||| Returns `Just` the given value if the conditional is `True`

42+||| and `Nothing` if the conditional is `False`.

39−toMaybe : Bool -> a -> Maybe a

43+toMaybe : Bool -> Lazy a -> Maybe a

40toMaybe True j = Just j

44toMaybe True j = Just j

41toMaybe False j = Nothing

45toMaybe False j = Nothing

42

46

43justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

47justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

44justInjective refl = refl

48justInjective refl = refl

45

49

50+||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case

51+||| that the `Maybe` value is `Nothing`.

46lowerMaybe : Monoid a => Maybe a -> a

52lowerMaybe : Monoid a => Maybe a -> a

47lowerMaybe Nothing = neutral

53lowerMaybe Nothing = neutral

48lowerMaybe (Just x) = x

54lowerMaybe (Just x) = x

49

55

56+||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.

50raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

57raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

51raiseToMaybe x = if x == neutral then Nothing else Just x

58raiseToMaybe x = if x == neutral then Nothing else Just x

52

59

libs/prelude/Prelude/Stream.idr+3−1

@@ -31,8 +31,10 @@ take : (n : Nat) -> (xs : Stream a) -> Vect n a

31take Z _ = []

32take (S n) (x :: xs) = x :: (take n xs)

33

34+||| Drop the first n elements from the stream

35+||| @ n how many elements to drop

34%assert_total

36%assert_total

35−drop : Nat -> Stream a -> Stream a

37+drop : (n : Nat) -> Stream a -> Stream a

36drop Z xs = xs

38drop Z xs = xs

37drop (S k) (x::xs) = drop k xs

39drop (S k) (x::xs) = drop k xs

38

40

libs/prelude/Prelude/Vect.idr+19

@@ -447,6 +447,25 @@ range : Vect n (Fin n)

447range {n=Z} = []

448range {n=S _} = fZ :: map fS range

449

450+

451+--------------------------------------------------------------------------------

452+-- Properties

453+--------------------------------------------------------------------------------

454+

455+vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)

456+vectConsCong x xs xs refl = refl

457+

458+vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

459+vectNilRightNeutral [] = refl

460+vectNilRightNeutral (x :: xs) =

461+ vectConsCong _ _ _ (vectNilRightNeutral xs)

462+

463+vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z

464+vectAppendAssociative [] y z = refl

465+vectAppendAssociative (x :: xs) ys zs =

466+ vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

467+

468+

450--------------------------------------------------------------------------------

469--------------------------------------------------------------------------------

451-- Proofs

470-- Proofs

452--------------------------------------------------------------------------------

471--------------------------------------------------------------------------------

src/IRTS/CodegenJavaScript.hs+21−8

@@ -1424,17 +1424,30 @@ elimConds js =

1424 isCond :: JS -> Bool

1425 isCond (JSAlloc

1426 fun (Just (JSFunction args (JSCond

1427− [ (JSBinOp "==" (JSNum (JSInt tag)) _, JSReturn (JSIdent _))

1427+ [ (JSBinOp "==" (JSNum (JSInt tag)) (JSProj (JSIdent _) "tag"), JSReturn t)

1428− , (JSNoop, JSReturn (JSIdent _))

1428+ , (JSNoop, JSReturn f)

1429− ]))

1429+ ])))

1430+ )

1431+ | isJSConstant t && isJSConstant f =

1432+ True

1433+

1434+ | JSIdent _ <- t

1435+ , JSIdent _ <- f =

1430− )) = True

1436+ True

1431

1437

1432 isCond (JSAlloc

1438 isCond (JSAlloc

1433 fun (Just (JSFunction args (JSCond

1439 fun (Just (JSFunction args (JSCond

1434− [ (JSBinOp "==" _ (JSNum (JSInt tag)), JSReturn (JSIdent _))

1440+ [ (JSBinOp "==" (JSIdent _) c, JSReturn t)

1435− , (JSNoop, JSReturn (JSIdent _))

1441+ , (JSNoop, JSReturn f)

1436− ]))

1442+ ])))

1443+ )

1444+ | isJSConstant t && isJSConstant f && isJSConstant c =

1445+ True

1446+

1447+ | JSIdent _ <- t

1448+ , JSIdent _ <- f

1449+ , isJSConstant c =

1437− )) = True

1450+ True

1438

1451

1439 isCond _ = False

1452 isCond _ = False

1440

1453

src/IRTS/Compiler.hs+7−2

@@ -52,6 +52,7 @@ import Paths_idris

52compile :: Codegen -> FilePath -> Term -> Idris ()

53compile codegen f tm

54 = do checkMVs -- check for undefined metavariables

55+ checkTotality -- refuse to compile if there are totality problems

55 reachableNames <- performUsageAnalysis

56 reachableNames <- performUsageAnalysis

56 maindef <- irMain tm

57 maindef <- irMain tm

57 iLOG $ "MAIN: " ++ show maindef

58 iLOG $ "MAIN: " ++ show maindef

@@ -105,6 +106,10 @@ compile codegen f tm

105 case map fst (idris_metavars i) \\ primDefs of

106 case map fst (idris_metavars i) \\ primDefs of

106 [] -> return ()

107 [] -> return ()

107 ms -> ifail $ "There are undefined metavariables: " ++ show ms

108 ms -> ifail $ "There are undefined metavariables: " ++ show ms

109+ checkTotality = do i <- getIState

110+ case idris_totcheckfail i of

111+ [] -> return ()

112+ ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg

108 inDir d h = do let f = d </> h

113 inDir d h = do let f = d </> h

109 ex <- doesFileExist f

114 ex <- doesFileExist f

110 if ex then return f else return h

115 if ex then return f else return h

@@ -249,8 +254,8 @@ irTerm vs env tm@(App f a) = case unApply tm of

249

254

250 -- This case is here until we get more general inlining. It's just

255 -- This case is here until we get more general inlining. It's just

251 -- a really common case, and the laziness hurts...

256 -- a really common case, and the laziness hurts...

252− (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),

257+ (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),

253− (App (P _ (UN d') _) e)])

258+ (App (App (App (P _ (UN d') _) _) _) e)])

254 | be == txt "boolElim"

259 | be == txt "boolElim"

255 , d == txt "Delay"

260 , d == txt "Delay"

256 , d' == txt "Delay"

261 , d' == txt "Delay"

src/Idris/ASTUtils.hs+40−21

@@ -25,7 +25,11 @@ module Idris.ASTUtils where

25-- fputState (detag n2) False

26--

27-- -- Note that all these operations handle missing items consistently

28−-- -- and transparently, as prescribed by the typeclass InitialValue.

28+-- -- and transparently, as prescribed by the default values included

29+-- -- in the definitions of the ist_* functions.

30+-- --

31+-- -- Especially, it's no longer necessary to have initial values of

32+-- -- data structures copied (possibly inconsistently) all over the compiler.

29

33

30import Control.Category

34import Control.Category

31import Control.Applicative

35import Control.Applicative

@@ -57,20 +61,22 @@ fputState field x = fmodifyState field (const x)

57fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()

61fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()

58fmodifyState field f = modify $ fmodify field f

62fmodifyState field f = modify $ fmodify field f

59

63

60−-- Until now, we'd have just ad-hoc empty lists and Falses thrown around

61−-- whenever a new instance of a record was to be created.

62−--

63−-- This class formalises the notion of an initial value for a record.

64−class InitialValue a where

65− initialValue :: a

66−

67−-- Exact-name context lookup; uses the initial value if needed.

64+-- Exact-name context lookup; uses Nothing for deleted values (read+write!).

65+--

66+-- Reading a non-existing value yields Nothing,

67+-- writing Nothing deletes the value (if it existed).

68−ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a

68+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)

69−ctxt_lookupExact n = Field

69+ctxt_lookup n = Field

70− { fget = fromMaybe initialValue . lookupCtxtExact n

70+ { fget = lookupCtxtExact n

71+ , fset = \newVal -> case newVal of

71− , fset = addDef n

72+ Just x -> addDef n x

73+ Nothing -> deleteDefExact n

72 }

74 }

73

75

76+-- Maybe-lens with a default value.

77+maybe_default :: a -> Field (Maybe a) a

78+maybe_default dflt = Field (fromMaybe dflt) (const . Just)

79+

74

80

75-----------------------------------

81-----------------------------------

76-- Individual records and fields --

82-- Individual records and fields --

@@ -83,12 +89,14 @@ ctxt_lookupExact n = Field

83-- OptInfo

89-- OptInfo

84----------

90----------

85

91

86−instance InitialValue OptInfo where

87− initialValue = Optimise [] False

88−

89-- the optimisation record for the given (exact) name

92-- the optimisation record for the given (exact) name

90ist_optimisation :: Name -> Field IState OptInfo

93ist_optimisation :: Name -> Field IState OptInfo

91−ist_optimisation n = ctxt_lookupExact n

94+ist_optimisation n =

95+ maybe_default Optimise

96+ { inaccessible = []

97+ , detaggable = False

98+ }

99+ . ctxt_lookup n

92 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

100 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

93

101

94-- two fields of the optimisation record

102-- two fields of the optimisation record

@@ -102,14 +110,25 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

102-- CGInfo

110-- CGInfo

103---------

111---------

104

112

105−instance InitialValue CGInfo where

106− initialValue = CGInfo [] [] [] [] []

107−

108-- callgraph record for the given (exact) name

113-- callgraph record for the given (exact) name

109ist_callgraph :: Name -> Field IState CGInfo

114ist_callgraph :: Name -> Field IState CGInfo

110−ist_callgraph n = ctxt_lookupExact n

115+ist_callgraph n =

116+ maybe_default CGInfo

117+ { argsdef = [], calls = [], scg = []

118+ , argsused = [], usedpos = []

119+ }

120+ . ctxt_lookup n

111 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

121 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

112

122

113-- some fields of the CGInfo record

123-- some fields of the CGInfo record

114cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

124cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

115cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

125cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

126+

127+

128+-- Commandline flags

129+--------------------

130+

131+opts_idrisCmdline :: Field IState [Opt]

132+opts_idrisCmdline =

133+ Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })

134+ . Field idris_options (\v ist -> ist{ idris_options = v })

src/Idris/AbsSyntax.hs+1−1

@@ -530,7 +530,7 @@ renderWidth = do iw <- getWidth

530

531

532type1Doc :: Doc OutputAnnotation

533−type1Doc = (annotate AnnConstType $ text "Type 1")

533+type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")

534

535

536isetPrompt :: String -> Idris ()

src/Idris/AbsSyntaxTree.hs+102−79

@@ -95,6 +95,28 @@ defaultOpts = IOption { opt_logLevel = 0

95 , opt_autoSolve = True

96 }

97

98+data PPOption = PPOption {

99+ ppopt_impl :: Bool -- ^^ whether to show implicits

100+} deriving (Show)

101+

102+-- | Pretty printing options with default verbosity.

103+defaultPPOption :: PPOption

104+defaultPPOption = PPOption { ppopt_impl = False }

105+

106+-- | Pretty printing options with the most verbosity.

107+verbosePPOption :: PPOption

108+verbosePPOption = PPOption { ppopt_impl = True }

109+

110+-- | Get pretty printing options from the big options record.

111+ppOption :: IOption -> PPOption

112+ppOption opt = PPOption {

113+ ppopt_impl = opt_showimp opt

114+}

115+

116+-- | Get pretty printing options from an idris state record.

117+ppOptionIst :: IState -> PPOption

118+ppOptionIst = ppOption . idris_options

119+

98data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

99

121

100-- | The output mode in use

122-- | The output mode in use

@@ -127,6 +149,7 @@ data IState = IState {

127 idris_tyinfodata :: Ctxt TIData,

149 idris_tyinfodata :: Ctxt TIData,

128 idris_totcheck :: [(FC, Name)], -- names to check totality on

150 idris_totcheck :: [(FC, Name)], -- names to check totality on

129 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

151 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

152+ idris_totcheckfail :: [(FC, String)],

130 idris_options :: IOption,

153 idris_options :: IOption,

131 idris_name :: Int,

154 idris_name :: Int,

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

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

@@ -231,6 +254,7 @@ data IBCWrite = IBCFix FixDecl

231 | IBCErrorHandler Name

254 | IBCErrorHandler Name

232 | IBCFunctionErrorHandler Name Name Name

255 | IBCFunctionErrorHandler Name Name Name

233 | IBCPostulate Name

256 | IBCPostulate Name

257+ | IBCTotCheckErr FC String

234 deriving Show

258 deriving Show

235

259

236-- | The initial state for the compiler

260-- | The initial state for the compiler

@@ -239,7 +263,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

239 emptyContext emptyContext emptyContext emptyContext

263 emptyContext emptyContext emptyContext emptyContext

240 emptyContext emptyContext emptyContext emptyContext

264 emptyContext emptyContext emptyContext emptyContext

241 emptyContext emptyContext

265 emptyContext emptyContext

242− [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

266+ [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

243 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

267 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

244 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

268 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

245 AutomaticWidth S.empty Nothing Nothing

269 AutomaticWidth S.empty Nothing Nothing

@@ -264,7 +288,7 @@ data Command = Quit

264 | Help

288 | Help

265 | Eval PTerm

289 | Eval PTerm

266 | Check PTerm

290 | Check PTerm

267− | DocStr Name

291+ | DocStr (Either Name Const)

268 | TotCheck Name

292 | TotCheck Name

269 | Reload

293 | Reload

270 | Load FilePath

294 | Load FilePath

@@ -297,9 +321,9 @@ data Command = Quit

297 | AddProofClauseFrom Bool Int Name

321 | AddProofClauseFrom Bool Int Name

298 | AddMissing Bool Int Name

322 | AddMissing Bool Int Name

299 | MakeWith Bool Int Name

323 | MakeWith Bool Int Name

300− | DoProofSearch Bool -- ^ update

324+ | DoProofSearch Bool Bool Int Name [Name]

301− Bool -- ^ recursive (i.e. do arguments too)

325+ -- ^ the first bool is whether to update,

302− Int Name [Name]

326+ -- the second is whether to search recursively (i.e. for the arguments)

303 | SetOpt Opt

327 | SetOpt Opt

304 | UnsetOpt Opt

328 | UnsetOpt Opt

305 | NOP

329 | NOP

@@ -717,8 +741,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

717 | MatchRefine Name

741 | MatchRefine Name

718 | LetTac Name t | LetTacTy Name t t

742 | LetTac Name t | LetTacTy Name t t

719 | Exact t | Compute | Trivial | TCInstance

743 | Exact t | Compute | Trivial | TCInstance

720− | ProofSearch Bool -- ^ recursive

721− (Maybe Name) [Name]

744+ | ProofSearch Bool (Maybe Name) [Name]

745+ -- ^ the bool is whether to search recursively

722 | Solve

746 | Solve

723 | Attack

747 | Attack

724 | ProofState | ProofTerm | Undo

748 | ProofState | ProofTerm | Undo

@@ -1089,29 +1113,31 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

1089-- could interfere with interactive editing, which calls "show".

1113-- could interfere with interactive editing, which calls "show".

1090

1114

1091instance Show PTerm where

1115instance Show PTerm where

1092− showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm

1116+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm

1093

1117

1094instance Show PDecl where

1118instance Show PDecl where

1095− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d

1119+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d

1096

1120

1097instance Show PClause where

1121instance Show PClause where

1098− showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c

1122+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c

1099

1123

1100instance Show PData where

1124instance Show PData where

1101− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d

1125+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d

1102

1126

1103instance Pretty PTerm OutputAnnotation where

1127instance Pretty PTerm OutputAnnotation where

1104− pretty = prettyImp False

1128+ pretty = prettyImp defaultPPOption

1105

1129

1106-- | Colourise annotations according to an Idris state. It ignores the names

1130-- | Colourise annotations according to an Idris state. It ignores the names

1107-- in the annotation, as there's no good way to show extended information on a

1131-- in the annotation, as there's no good way to show extended information on a

1108-- terminal.

1132-- terminal.

1109consoleDecorate :: IState -> OutputAnnotation -> String -> String

1133consoleDecorate :: IState -> OutputAnnotation -> String -> String

1110consoleDecorate ist _ | not (idris_colourRepl ist) = id

1134consoleDecorate ist _ | not (idris_colourRepl ist) = id

1111−consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist

1135+consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist

1136+ in if constIsType c

1137+ then colouriseType theme

1112− in colouriseData theme

1138+ else colouriseData theme

1113−consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1139+consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)

1114− in colouriseType theme

1140+consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)

1115consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1141consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1116consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1142consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1117consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1143consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

@@ -1129,23 +1155,23 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1129 colour ItalicText = IdrisColour Nothing True False False True

1155 colour ItalicText = IdrisColour Nothing True False False True

1130

1156

1131-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1157-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1132−prettyImp :: Bool -- ^^ whether to show implicits

1158+prettyImp :: PPOption -- ^^ pretty printing options

1133 -> PTerm -- ^^ the term to pretty-print

1159 -> PTerm -- ^^ the term to pretty-print

1134 -> Doc OutputAnnotation

1160 -> Doc OutputAnnotation

1135prettyImp impl = pprintPTerm impl [] [] []

1161prettyImp impl = pprintPTerm impl [] [] []

1136

1162

1137-- | Do the right thing for rendering a term in an IState

1163-- | Do the right thing for rendering a term in an IState

1138prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1164prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1139−prettyIst ist = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist)

1165+prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1140

1166

1141-- | Pretty-print a high-level Idris term in some bindings context with infix info

1167-- | Pretty-print a high-level Idris term in some bindings context with infix info

1142−pprintPTerm :: Bool -- ^^ whether to show implicits

1168+pprintPTerm :: PPOption -- ^^ pretty printing options

1143 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1169 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1144 -> [Name] -- ^^ names to always show in pi, even if not used

1170 -> [Name] -- ^^ names to always show in pi, even if not used

1145 -> [FixDecl] -- ^^ Fixity declarations

1171 -> [FixDecl] -- ^^ Fixity declarations

1146 -> PTerm -- ^^ the term to pretty-print

1172 -> PTerm -- ^^ the term to pretty-print

1147 -> Doc OutputAnnotation

1173 -> Doc OutputAnnotation

1148−pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1174+pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1149 where

1175 where

1150 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1176 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1151 prettySe p bnd (PQuote r) =

1177 prettySe p bnd (PQuote r) =

@@ -1153,8 +1179,8 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1153 prettySe p bnd (PPatvar fc n) = pretty n

1179 prettySe p bnd (PPatvar fc n) = pretty n

1154 prettySe p bnd e

1180 prettySe p bnd e

1155 | Just str <- slist p bnd e = str

1181 | Just str <- slist p bnd e = str

1156− | Just n <- snat p e = annotate AnnConstData (text (show n))

1182+ | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1157− prettySe p bnd (PRef fc n) = prettyName impl bnd n

1183+ prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n

1158 prettySe p bnd (PLam n ty sc) =

1184 prettySe p bnd (PLam n ty sc) =

1159 bracket p 2 . group . align . hang 2 $

1185 bracket p 2 . group . align . hang 2 $

1160 text "\\" <> bindingOf n False <+> text "=>" <$>

1186 text "\\" <> bindingOf n False <+> text "=>" <$>

@@ -1165,20 +1191,20 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1165 prettySe 10 bnd v <+> kwd "in" </>

1191 prettySe 10 bnd v <+> kwd "in" </>

1166 prettySe 10 ((n, False):bnd) sc

1192 prettySe 10 ((n, False):bnd) sc

1167 prettySe p bnd (PPi (Exp l s _) n ty sc)

1193 prettySe p bnd (PPi (Exp l s _) n ty sc)

1168− | n `elem` allNamesIn sc || impl || n `elem` docArgs =

1194+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1169 bracket p 2 . group $

1195 bracket p 2 . group $

1170 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1196 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1171 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1197 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1172 | otherwise =

1198 | otherwise =

1173 bracket p 2 . group $

1199 bracket p 2 . group $

1174− group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1200+ group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1175 where

1201 where

1176 st =

1202 st =

1177 case s of

1203 case s of

1178 Static -> text "[static]" <> space

1204 Static -> text "[static]" <> space

1179 _ -> empty

1205 _ -> empty

1180 prettySe p bnd (PPi (Imp l s _) n ty sc)

1206 prettySe p bnd (PPi (Imp l s _) n ty sc)

1181− | impl =

1207+ | ppopt_impl ppo =

1182 bracket p 2 $

1208 bracket p 2 $

1183 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1209 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1184 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1210 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1197,16 +1223,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1197 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1223 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1198 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1224 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1199 | UN nm <- basename f

1225 | UN nm <- basename f

1226+ , not (ppopt_impl ppo) && null (getExps args) =

1200− , not impl && null (getExps args) = if isAlpha (thead nm)

1227+ if isAlpha (thead nm)

1201− then prettyName impl bnd f

1228+ then prettyName (ppopt_impl ppo) bnd f

1202− else enclose lparen rparen $

1229+ else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f

1203− prettyName impl bnd f

1204 prettySe p bnd (PAppBind _ (PRef _ f) [])

1230 prettySe p bnd (PAppBind _ (PRef _ f) [])

1205− | not impl = text "!" <> prettyName impl bnd f

1231+ | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f

1206− prettySe p bnd (PApp _ (PRef _ op) args)

1232+ prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators

1207 | UN nm <- basename op

1233 | UN nm <- basename op

1208 , not (tnull nm) &&

1234 , not (tnull nm) &&

1209− (not impl) && (not $ isAlpha (thead nm)) =

1235+ (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1210 case getExps args of

1236 case getExps args of

1211 [] -> enclose lparen rparen opName

1237 [] -> enclose lparen rparen opName

1212 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1238 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

@@ -1215,7 +1241,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1215 (l:r:rest) -> bracket p 1 $

1241 (l:r:rest) -> bracket p 1 $

1216 enclose lparen rparen (inFix l r) <+>

1242 enclose lparen rparen (inFix l r) <+>

1217 align (group (vsep (map (prettyArgSe bnd) rest)))

1243 align (group (vsep (map (prettyArgSe bnd) rest)))

1218− where opName = prettyName impl bnd op

1244+ where opName = prettyName (ppopt_impl ppo) bnd op

1219 f = getFixity (opStr op)

1245 f = getFixity (opStr op)

1220 left l = case f of

1246 left l = case f of

1221 Nothing -> prettySe (-1) bnd l

1247 Nothing -> prettySe (-1) bnd l

@@ -1227,15 +1253,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1227 Just f' -> prettySe (prec f'-1) bnd r

1253 Just f' -> prettySe (prec f'-1) bnd r

1228 inFix l r = align . group $

1254 inFix l r = align . group $

1229 (left l <+> opName) <$> group (right r)

1255 (left l <+> opName) <$> group (right r)

1230− prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1256+ prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1231 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1257 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1258+ f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1232− f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1259+ char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1233− prettySe p bnd (PApp _ f as) =

1260+ prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1234 let args = getExps as

1261 let args = getExps as

1235 fp = prettySe 1 bnd f

1262 fp = prettySe 1 bnd f

1236 in

1263 in

1237 bracket p 1 . group $

1264 bracket p 1 . group $

1238− if impl

1265+ if ppopt_impl ppo

1239 then if null as

1266 then if null as

1240 then fp

1267 then fp

1241 else fp <+> align (vsep (map (prettyArgS bnd) as))

1268 else fp <+> align (vsep (map (prettyArgS bnd) as))

@@ -1297,13 +1324,8 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1297 where

1324 where

1298 prettyAs =

1325 prettyAs =

1299 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1326 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1300− prettySe p bnd PType = annotate AnnConstType $ text "Type"

1327+ prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1301− prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))

1328+ prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1302− where annot (AType _) = AnnConstType

1303− annot StrType = AnnConstType

1304− annot PtrType = AnnConstType

1305− annot VoidType = AnnConstType

1306− annot _ = AnnConstData

1307 -- XXX: add pretty for tactics

1329 -- XXX: add pretty for tactics

1308 prettySe p bnd (PProof ts) =

1330 prettySe p bnd (PProof ts) =

1309 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1331 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

@@ -1340,9 +1362,9 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1340 basename n = n

1362 basename n = n

1341

1363

1342 slist' p bnd (PApp _ (PRef _ nil) _)

1364 slist' p bnd (PApp _ (PRef _ nil) _)

1343− | not impl && nsroot nil == sUN "Nil" = Just []

1365+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1344 slist' p bnd (PRef _ nil)

1366 slist' p bnd (PRef _ nil)

1345− | not impl && nsroot nil == sUN "Nil" = Just []

1367+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1346 slist' p bnd (PApp _ (PRef _ cons) args)

1368 slist' p bnd (PApp _ (PRef _ cons) args)

1347 | nsroot cons == sUN "::",

1369 | nsroot cons == sUN "::",

1348 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1370 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

@@ -1355,16 +1377,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1355 slist' _ _ tm = Nothing

1377 slist' _ _ tm = Nothing

1356

1378

1357 slist p bnd e | Just es <- slist' p bnd e = Just $

1379 slist p bnd e | Just es <- slist' p bnd e = Just $

1358− case es of [] -> annotate AnnConstData $ text "[]"

1380+ case es of [] -> annotate (AnnData "" "") $ text "[]"

1359 [x] -> enclose left right . group $

1381 [x] -> enclose left right . group $

1360 prettySe p bnd x

1382 prettySe p bnd x

1361 xs -> (enclose left right .

1383 xs -> (enclose left right .

1362 align . group . vsep .

1384 align . group . vsep .

1363 punctuate comma .

1385 punctuate comma .

1364 map (prettySe p bnd)) xs

1386 map (prettySe p bnd)) xs

1365− where left = (annotate AnnConstData (text "["))

1387+ where left = (annotate (AnnData "" "") (text "["))

1366− right = (annotate AnnConstData (text "]"))

1388+ right = (annotate (AnnData "" "") (text "]"))

1367− comma = (annotate AnnConstData (text ","))

1389+ comma = (annotate (AnnData "" "") (text ","))

1368 slist _ _ _ = Nothing

1390 slist _ _ _ = Nothing

1369

1391

1370 pairElts :: PTerm -> Maybe [PTerm]

1392 pairElts :: PTerm -> Maybe [PTerm]

@@ -1415,43 +1437,43 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

1415 strName other = show other

1437 strName other = show other

1416

1438

1417

1439

1418−showCImp :: Bool -> PClause -> Doc OutputAnnotation

1440+showCImp :: PPOption -> PClause -> Doc OutputAnnotation

1419−showCImp impl (PClause _ n l ws r w)

1441+showCImp ppo (PClause _ n l ws r w)

1420− = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

1442+ = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r

1421 <+> text "where" <+> text (show w)

1443 <+> text "where" <+> text (show w)

1422 where

1444 where

1423 showWs [] = empty

1445 showWs [] = empty

1424− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1446+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1425−showCImp impl (PWith _ n l ws r w)

1447+showCImp ppo (PWith _ n l ws r w)

1426− = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

1448+ = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

1427 <+> braces (text (show w))

1449 <+> braces (text (show w))

1428 where

1450 where

1429 showWs [] = empty

1451 showWs [] = empty

1430− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1452+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1431

1453

1432

1454

1433−showDImp :: Bool -> PData -> Doc OutputAnnotation

1455+showDImp :: PPOption -> PData -> Doc OutputAnnotation

1434−showDImp impl (PDatadecl n ty cons)

1456+showDImp ppo (PDatadecl n ty cons)

1435− = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1457+ = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>

1436− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1458+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))

1437

1459

1438−showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1460+showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

1439−showDecls i ds = vsep (map (showDeclImp i) ds)

1461+showDecls o ds = vsep (map (showDeclImp o) ds)

1440

1462

1441showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1463showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1442−showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1464+showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1443−showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1465+showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1444− indent 2 (vsep (map (showCImp i) cs))

1466+ indent 2 (vsep (map (showCImp o) cs))

1445−showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1467+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

1446−showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

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

1447−showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

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

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

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

1449−showDeclImp i (PClass _ _ _ cs n ps _ ds)

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

1450− = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

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

1451−showDeclImp i (PInstance _ _ cs n _ t _ ds)

1473+showDeclImp o (PInstance _ _ cs n _ t _ ds)

1452− = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

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

1453showDeclImp _ _ = text "..."

1475showDeclImp _ _ = text "..."

1454−-- showDeclImp (PImport i) = "import " ++ i

1476+-- showDeclImp (PImport o) = "import " ++ o

1455

1477

1456instance Show (Doc OutputAnnotation) where

1478instance Show (Doc OutputAnnotation) where

1457 show = flip (displayS . renderCompact) ""

1479 show = flip (displayS . renderCompact) ""

@@ -1478,14 +1500,14 @@ getAll = map getTm

1478-- | Show Idris name

1500-- | Show Idris name

1479showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1501showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1480 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1502 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1481− -> Bool -- ^^ whether to show implicits

1503+ -> PPOption -- ^^ pretty printing options

1482 -> Bool -- ^^ whether to colourise

1504 -> Bool -- ^^ whether to colourise

1483 -> Name -- ^^ the term to show

1505 -> Name -- ^^ the term to show

1484 -> String

1506 -> String

1485−showName ist bnd impl colour n = case ist of

1507+showName ist bnd ppo colour n = case ist of

1486 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1508 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1487 Nothing -> showbasic n

1509 Nothing -> showbasic n

1488− where name = if impl then show n else showbasic n

1510+ where name = if ppopt_impl ppo then show n else showbasic n

1489 showbasic n@(UN _) = showCG n

1511 showbasic n@(UN _) = showCG n

1490 showbasic (MN _ s) = str s

1512 showbasic (MN _ s) = str s

1491 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

1513 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

@@ -1509,11 +1531,12 @@ showTm :: IState -- ^^ the Idris state, for information about identifiers and co

1509 -> String

1531 -> String

1510showTm ist = displayDecorated (consoleDecorate ist) .

1532showTm ist = displayDecorated (consoleDecorate ist) .

1511 renderPretty 0.8 100000 .

1533 renderPretty 0.8 100000 .

1512− prettyImp (opt_showimp (idris_options ist))

1534+ prettyImp (ppOptionIst ist)

1513

1535

1514-- | Show a term with implicits, no colours

1536-- | Show a term with implicits, no colours

1515showTmImpls :: PTerm -> String

1537showTmImpls :: PTerm -> String

1516−showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

1538+showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

1539+

1517

1540

1518

1541

1519instance Sized PTerm where

1542instance Sized PTerm where

src/Idris/Apropos.hs+12−8

@@ -9,8 +9,8 @@ import Idris.Docstrings (Docstring, containsText)

9import Data.List (nub)

10import qualified Data.Text as T

11

12−-- | Find definitions that are relevant to some string. Relevance is one or

12+-- | Find definitions that are relevant to all space-delimited components of

13−-- more of the following:

13+-- some string. Relevance is one or more of the following:

14--

15-- * the string is a substring of the name

16--

@@ -20,8 +20,12 @@ import qualified Data.Text as T

20apropos :: IState -> T.Text -> [Name]

21apropos ist what = let defs = ctxtAlist (tt_ctxt ist)

22 docs = toAlist (idris_docstrings ist)

23− in nub (map fst (filter (isApropos what) defs) ++

23+ in nub (map fst (isAproposAll parts defs) ++

24− map fst (filter (isApropos what) docs))

24+ map fst (isAproposAll parts docs))

25+ where isAproposAll [] xs = xs

26+ isAproposAll (what:more) xs = filter (isApropos what)

27+ (isAproposAll more xs)

28+ parts = filter ((> 0) . T.length) . T.splitOn (T.pack " ") $ what

25

29

26textIn :: T.Text -> T.Text -> Bool

30textIn :: T.Text -> T.Text -> Bool

27textIn a b = T.isInfixOf (T.toLower a) (T.toLower b)

31textIn a b = T.isInfixOf (T.toLower a) (T.toLower b)

@@ -48,10 +52,10 @@ instance Apropos Def where

48 isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty

52 isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty

49

53

50instance Apropos (Binder (TT Name)) where

54instance Apropos (Binder (TT Name)) where

51− isApropos str (Lam ty) = isApropos str ty

55+ isApropos str (Lam ty) = str == T.pack "\\" || isApropos str ty

52− isApropos str (Pi ty) = isApropos str ty

56+ isApropos str (Pi ty) = str == T.pack "->" || isApropos str ty

53− isApropos str (Let ty val) = isApropos str ty || isApropos str val

57+ isApropos str (Let ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

54− isApropos str (NLet ty val) = isApropos str ty || isApropos str val

58+ isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

55 isApropos str _ = False -- these shouldn't occur in defined libraries

59 isApropos str _ = False -- these shouldn't occur in defined libraries

56

60

57instance Apropos (TT Name) where

61instance Apropos (TT Name) where

src/Idris/Core/TC.hs+9

@@ -2,6 +2,7 @@

2

3module Idris.Core.TC(TC'(..)) where

4

5+import Control.Applicative

5import Control.Monad

6import Control.Monad

6import Control.Monad.Trans.Error(Error(..))

7import Control.Monad.Trans.Error(Error(..))

7

8

@@ -26,3 +27,11 @@ instance Error e => MonadPlus (TC' e) where

26 _ `mplus` (OK y) = OK y

27 _ `mplus` (OK y) = OK y

27 err `mplus` _ = err

28 err `mplus` _ = err

28

29

30+

31+instance Error e => Applicative (TC' e) where

32+ pure = return

33+ (<*>) = ap

34+

35+instance Error e => Alternative (TC' e) where

36+ empty = mzero

37+ (<|>) = mplus

src/Idris/Core/TT.hs+61−2

@@ -27,6 +27,7 @@ import Control.Monad.Trans.Error (Error(..))

27import Debug.Trace

28import qualified Data.Map.Strict as Map

29import Data.Char

30+import Numeric (showIntAtBase)

30import qualified Data.Text as T

31import qualified Data.Text as T

31import Data.List

32import Data.List

32import Data.Maybe (listToMaybe)

33import Data.Maybe (listToMaybe)

@@ -92,8 +93,9 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

92 -- ^^ The name, classification, docs overview, and pretty-printed type

93 -- ^^ The name, classification, docs overview, and pretty-printed type

93 | AnnBoundName Name Bool

94 | AnnBoundName Name Bool

94 -- ^^ The name and whether it is implicit

95 -- ^^ The name and whether it is implicit

95− | AnnConstData

96+ | AnnConst Const

96− | AnnConstType

97+ | AnnData String String -- ^ type, doc overview

98+ | AnnType String String -- ^ name, doc overview

97 | AnnKeyword

99 | AnnKeyword

98 | AnnFC FC

100 | AnnFC FC

99 | AnnTextFmt TextFormatting

101 | AnnTextFmt TextFormatting

@@ -426,6 +428,9 @@ lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)

426lookupCtxtExact :: Name -> Ctxt a -> Maybe a

428lookupCtxtExact :: Name -> Ctxt a -> Maybe a

427lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

429lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

428

430

431+deleteDefExact :: Name -> Ctxt a -> Ctxt a

432+deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)

433+

429updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

434updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

430updateDef n f ctxt

435updateDef n f ctxt

431 = let ds = lookupCtxtName n ctxt in

436 = let ds = lookupCtxtName n ctxt in

@@ -521,6 +526,60 @@ instance Pretty Const OutputAnnotation where

521 pretty (B32 w) = text . show $ w

526 pretty (B32 w) = text . show $ w

522 pretty (B64 w) = text . show $ w

527 pretty (B64 w) = text . show $ w

523

528

529+-- | Determines whether the input constant represents a type

530+constIsType :: Const -> Bool

531+constIsType (I _) = False

532+constIsType (BI _) = False

533+constIsType (Fl _) = False

534+constIsType (Ch _) = False

535+constIsType (Str _) = False

536+constIsType (B8 _) = False

537+constIsType (B16 _) = False

538+constIsType (B32 _) = False

539+constIsType (B64 _) = False

540+constIsType (B8V _) = False

541+constIsType (B16V _) = False

542+constIsType (B32V _) = False

543+constIsType (B64V _) = False

544+constIsType _ = True

545+

546+-- | Get the docstring for a Const

547+constDocs :: Const -> String

548+constDocs c@(AType (ATInt ITBig)) = "Arbitrary-precision integers"

549+constDocs c@(AType (ATInt ITNative)) = "Fixed-precision integers of undefined size"

550+constDocs c@(AType (ATInt ITChar)) = "Characters in some unspecified encoding"

551+constDocs c@(AType ATFloat) = "Double-precision floating-point numbers"

552+constDocs StrType = "Strings in some unspecified encoding"

553+constDocs PtrType = "Foreign pointers"

554+constDocs ManagedPtrType = "Managed pointers"

555+constDocs BufferType = "Copy-on-write buffers"

556+constDocs c@(AType (ATInt (ITFixed IT8))) = "Eight bits (unsigned)"

557+constDocs c@(AType (ATInt (ITFixed IT16))) = "Sixteen bits (unsigned)"

558+constDocs c@(AType (ATInt (ITFixed IT32))) = "Thirty-two bits (unsigned)"

559+constDocs c@(AType (ATInt (ITFixed IT64))) = "Sixty-four bits (unsigned)"

560+constDocs c@(AType (ATInt (ITVec IT8 16))) = "Vectors of sixteen eight-bit values"

561+constDocs c@(AType (ATInt (ITVec IT16 8))) = "Vectors of eight sixteen-bit values"

562+constDocs c@(AType (ATInt (ITVec IT32 4))) = "Vectors of four thirty-two-bit values"

563+constDocs c@(AType (ATInt (ITVec IT64 2))) = "Vectors of two sixty-four-bit values"

564+constDocs (Fl f) = "A float"

565+constDocs (I i) = "A fixed-precision integer"

566+constDocs (BI i) = "An arbitrary-precision integer"

567+constDocs (Str s) = "A string of length " ++ show (length s)

568+constDocs (Ch c) = "A character"

569+constDocs (B8 w) = "The eight-bit value 0x" ++

570+ showIntAtBase 16 intToDigit w ""

571+constDocs (B16 w) = "The sixteen-bit value 0x" ++

572+ showIntAtBase 16 intToDigit w ""

573+constDocs (B32 w) = "The thirty-two-bit value 0x" ++

574+ showIntAtBase 16 intToDigit w ""

575+constDocs (B64 w) = "The sixty-four-bit value 0x" ++

576+ showIntAtBase 16 intToDigit w ""

577+constDocs (B8V v) = "A vector of eight-bit values"

578+constDocs (B16V v) = "A vector of sixteen-bit values"

579+constDocs (B32V v) = "A vector of thirty-two-bit values"

580+constDocs (B64V v) = "A vector of sixty-four-bit values"

581+constDocs prim = "Undocumented"

582+

524data Raw = Var Name

583data Raw = Var Name

525 | RBind Name (Binder Raw) Raw

584 | RBind Name (Binder Raw) Raw

526 | RApp Raw Raw

585 | RApp Raw Raw

src/Idris/Coverage.hs+12−8

@@ -9,7 +9,7 @@ import Idris.Core.CaseTree

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12−import Idris.Output (iputStrLn)

12+import Idris.Output (iWarn)

13

14import Data.List

15import Data.Either

@@ -253,9 +253,10 @@ checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

253checkAllCovering fc done top n | not (n `elem` done)

254 = do i <- get

255 case lookupTotal n (tt_ctxt i) of

256− [tot@(Partial NotCovering)] ->

256+ [tot@(Partial NotCovering)] ->

257− tclift $ tfail (At fc (Msg (show top ++ " is " ++ show tot

257+ do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

258− ++ " due to " ++ show n)))

258+ addIBC (IBCTotCheckErr fc msg)

259+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

259 _ -> return ()

260 _ -> return ()

260 case lookupCtxt n (idris_callgraph i) of

261 case lookupCtxt n (idris_callgraph i) of

261 [cg] -> mapM_ (checkAllCovering fc (n : done) top)

262 [cg] -> mapM_ (checkAllCovering fc (n : done) top)

@@ -388,18 +389,21 @@ checkTotality path fc n

388 Productive -> return t'

389 Productive -> return t'

389 e -> do w <- cmdOptType WarnPartial

390 e -> do w <- cmdOptType WarnPartial

390 if TotalFn `elem` opts

391 if TotalFn `elem` opts

391− then totalityError t'

392+ then do totalityError t'; return t'

392 else do when (w && not (PartialFn `elem` opts)) $

393 else do when (w && not (PartialFn `elem` opts)) $

393 warnPartial n t'

394 warnPartial n t'

394 return t'

395 return t'

395 where

396 where

396− totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

397+ totalityError t = do i <- getIState

398+ let msg = show n ++ " is " ++ show t

399+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}

400+ addIBC (IBCTotCheckErr fc msg)

397

401

398 warnPartial n t

402 warnPartial n t

399 = do i <- getIState

403 = do i <- getIState

400 case lookupDef n (tt_ctxt i) of

404 case lookupDef n (tt_ctxt i) of

401 [x] -> do

405 [x] -> do

402− iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t

406+ iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t

403-- ++ "\n" ++ show x

407-- ++ "\n" ++ show x

404-- let cg = lookupCtxtName Nothing n (idris_callgraph i)

408-- let cg = lookupCtxtName Nothing n (idris_callgraph i)

405-- iputStrLn (show cg)

409-- iputStrLn (show cg)

@@ -410,7 +414,7 @@ checkDeclTotality (fc, n)

410 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

414 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

411-- buildSCG (fc, n)

415-- buildSCG (fc, n)

412-- logLvl 2 $ "Built SCG"

416-- logLvl 2 $ "Built SCG"

413− i <- getIState

417+ i <- getIState

414 t <- checkTotality [] fc n

418 t <- checkTotality [] fc n

415 case t of

419 case t of

416 -- if it's not total, it can't reduce, to keep

420 -- if it's not total, it can't reduce, to keep

src/Idris/Delaborate.hs+2−2

@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

138pprintTerm ist = pprintTerm' ist []

139

140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141−pprintTerm' ist bnd = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist)

141+pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

142

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

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

@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>

269

270

271showqual :: IState -> Name -> String

272−showqual i n = showName (Just i) [] False False (dens n)

272+showqual i n = showName (Just i) [] (ppOptionIst i) { ppopt_impl = False } False (dens n)

273 where

274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of

275 [_] -> n -- just one thing

src/Idris/Docs.hs+25−12

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs (pprintDocs, getDocs, FunDoc(..), Docs (..)) where

2+module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where

3

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

@@ -37,8 +37,8 @@ showDoc d | nullDocstring d = empty

37

38pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

39pprintFD ist (FD n doc args ty f)

40− = nest 4 (prettyName imp [] n <+> colon <+>

40+ = nest 4 (prettyName (ppopt_impl ppo) [] n <+> colon <+>

41− pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args

41+ pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

42 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

43 renderDocstring doc <$>

44 maybe empty (\f -> text (show f) <> line) f <>

@@ -47,23 +47,23 @@ pprintFD ist (FD n doc args ty f)

47 then nest 4 $ text "Arguments:" <$> vsep argshow

48 else empty)

49

50− where imp = opt_showimp (idris_options ist)

50+ where ppo = ppOptionIst ist

51 infixes = idris_infixes ist

52 showArgs ((n, ty, Exp {}, Just d):args) bnd

53 = bindingOf n False <+> colon <+>

54− pprintPTerm imp bnd [] infixes ty <>

54+ pprintPTerm ppo bnd [] infixes ty <>

55 showDoc d <> line

56 :

57 showArgs args ((n, False):bnd)

58 showArgs ((n, ty, Constraint {}, Just d):args) bnd

59 = text "Class constraint" <+>

60− pprintPTerm imp bnd [] infixes ty <> showDoc d <> line

60+ pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line

61 :

62 showArgs args ((n, True):bnd)

63 showArgs ((n, ty, Imp {}, Just d):args) bnd

64 = text "(implicit)" <+>

65 bindingOf n True <+> colon <+>

66− pprintPTerm imp bnd [] infixes ty <>

66+ pprintPTerm ppo bnd [] infixes ty <>

67 showDoc d <> line

68 :

69 showArgs args ((n, True):bnd)

@@ -75,10 +75,11 @@ pprintDocs :: IState -> Docs -> Doc OutputAnnotation

75pprintDocs ist (FunDoc d) = pprintFD ist d

76pprintDocs ist (DataDoc t args)

77 = text "Data type" <+> pprintFD ist t <$>

78+ if null args then text "No constructors."

78− nest 4 (text "Constructors:" <> line <>

79+ else nest 4 (text "Constructors:" <> line <>

79− vsep (map (pprintFD ist) args))

80+ vsep (map (pprintFD ist) args))

80pprintDocs ist (ClassDoc n doc meths params instances superclasses)

81pprintDocs ist (ClassDoc n doc meths params instances superclasses)

81− = nest 4 (text "Type class" <+> prettyName imp [] n <>

82+ = nest 4 (text "Type class" <+> prettyName (ppopt_impl ppo) [] n <>

82 if nullDocstring doc then empty else line <> renderDocstring doc)

83 if nullDocstring doc then empty else line <> renderDocstring doc)

83 <> line <$>

84 <> line <$>

84 nest 4 (text "Parameters:" <$> prettyParameters)

85 nest 4 (text "Parameters:" <$> prettyParameters)

@@ -102,11 +103,11 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

102

103

103 pNames = map fst params

104 pNames = map fst params

104

105

105− imp = opt_showimp (idris_options ist)

106+ ppo = ppOptionIst ist

106 infixes = idris_infixes ist

107 infixes = idris_infixes ist

107

108

108 dumpInstance :: PTerm -> Doc OutputAnnotation

109 dumpInstance :: PTerm -> Doc OutputAnnotation

109− dumpInstance = pprintPTerm imp params' [] infixes

110+ dumpInstance = pprintPTerm ppo params' [] infixes

110

111

111 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

112 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

112 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

113 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

@@ -188,3 +189,15 @@ getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Do

188getPArgNames (PPi plicity name ty body) ds =

189getPArgNames (PPi plicity name ty body) ds =

189 (name, ty, plicity, lookup name ds) : getPArgNames body ds

190 (name, ty, plicity, lookup name ds) : getPArgNames body ds

190getPArgNames _ _ = []

191getPArgNames _ _ = []

192+

193+pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation

194+pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>

195+ pprintPTerm (ppOptionIst ist) [] [] [] (PConstant c) <+> colon <+>

196+ pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>

197+ nest 4 (line <> text str)

198+

199+ where t (Fl _) = PConstant $ AType ATFloat

200+ t (BI _) = PConstant $ AType (ATInt ITBig)

201+ t (Str _) = PConstant StrType

202+ t (Ch c) = PConstant $ AType (ATInt ITChar)

203+ t _ = PType

src/Idris/ElabDecls.hs+32−11

@@ -393,7 +393,7 @@ elabEliminator paramPos n ty cons info = do

393 elimLog elimSig

394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

396− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

396+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

398 -- Do not elaborate clauses if there aren't any

399 case eliminatorClauses of

@@ -774,11 +774,16 @@ elabTransform info fc safe lhs_in rhs_in

774

775elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

776 PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()

777−elabRecord info syn doc fc tyn ty opts cdoc cn cty

777+elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

778− = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

778+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])

779 -- TODO think: something more in info?

780− cty' <- implicit info syn cn cty

780+ cty' <- implicit info syn cn cty_in

781 i <- getIState

782+

783+ -- get bound implicits and propagate to setters (in case they

784+ -- provide useful information for inference)

785+ let extraImpls = getBoundImpls cty'

786+

782 cty <- case lookupTy cn (tt_ctxt i) of

787 cty <- case lookupTy cn (tt_ctxt i) of

783 [t] -> return (delab i t)

788 [t] -> return (delab i t)

784 _ -> ifail "Something went inexplicably wrong"

789 _ -> ifail "Something went inexplicably wrong"

@@ -797,14 +802,18 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

797 logLvl 1 $ show (recty, ptys)

802 logLvl 1 $ show (recty, ptys)

798 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)

803 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)

799 [pexp (PRef fc rec)])) ptys

804 [pexp (PRef fc rec)])) ptys

805+

806+ -- Generate projection functions

800 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

807 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

801 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

808 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

802 let implBinds = getImplB id cty'

809 let implBinds = getImplB id cty'

810+

811+ -- Generate update functions

803− update_decls <- mapM (mkUpdate recty index_names_in

812+ update_decls <- mapM (mkUpdate recty index_names_in extraImpls

804 (getFieldNames cty')

813 (getFieldNames cty')

805 implBinds (length nonImp)) (zip nonImp [0..])

814 implBinds (length nonImp)) (zip nonImp [0..])

806 mapM_ (elabDecl EAll info) (concat proj_decls)

815 mapM_ (elabDecl EAll info) (concat proj_decls)

807− logLvl 1 $ show update_decls

816+ logLvl 3 $ show update_decls

808 mapM_ (tryElabDecl info) (update_decls)

817 mapM_ (tryElabDecl info) (update_decls)

809 where

818 where

810-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

819-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

@@ -822,6 +831,9 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

822-- ++ "\n" ++ pshow i v

831-- ++ "\n" ++ pshow i v

823 putIState i)

832 putIState i)

824

833

834+ getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

835+ getBoundImpls _ = []

836+

825 getImplB k (PPi (Imp l s _) n Placeholder sc)

837 getImplB k (PPi (Imp l s _) n Placeholder sc)

826 = getImplB k sc

838 = getImplB k sc

827 getImplB k (PPi (Imp l s p) n ty sc)

839 getImplB k (PPi (Imp l s p) n ty sc)

@@ -886,7 +898,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

886 -- If the 'pty' we're updating includes anything in 'substs', we're

898 -- If the 'pty' we're updating includes anything in 'substs', we're

887 -- updating the type as well, so use recty', otherwise just use

899 -- updating the type as well, so use recty', otherwise just use

888 -- recty

900 -- recty

889− mkUpdate recty inames fnames k num ((pn, pty), pos)

901+ mkUpdate recty inames extras fnames k num ((pn, pty), pos)

890 = do let setname = expandNS syn $ mkType pn

902 = do let setname = expandNS syn $ mkType pn

891 let valname = sMN 0 "updateval"

903 let valname = sMN 0 "updateval"

892 let pn_out = sMN 0 (show pn ++ "_out")

904 let pn_out = sMN 0 (show pn ++ "_out")

@@ -894,8 +906,8 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

894 let recty_in = substMatches [(pn, PRef fc pn_in)] recty

906 let recty_in = substMatches [(pn, PRef fc pn_in)] recty

895 let recty_out = substMatches [(pn, PRef fc pn_out)] recty

907 let recty_out = substMatches [(pn, PRef fc pn_out)] recty

896 let pt = substMatches inames $

908 let pt = substMatches inames $

897− k (PPi expl pn_out pty

909+ k (implBindUp extras inames (PPi expl pn_out pty

898− (PPi expl rec recty_in recty_out))

910+ (PPi expl rec recty_in recty_out)))

899 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt

911 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt

900-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]

912-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]

901 let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames

913 let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames

@@ -913,6 +925,15 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

913 (map pexp rhsArgs)) []

925 (map pexp rhsArgs)) []

914 return (pn, pfnTy, PClauses fc [] setname [pclause])

926 return (pn, pfnTy, PClauses fc [] setname [pclause])

915

927

928+ implBindUp [] is t = t

929+ implBindUp ((n, ty):ns) is t

930+ = let n' = case lookup n is of

931+ Just (PRef _ x) -> x

932+ _ -> n in

933+ if n `elem` allNamesIn t

934+ then PPi impl n' ty (implBindUp ns is t)

935+ else implBindUp ns is t

936+

916-- FIXME: 'forcenames' is an almighty hack! Need a better way of

937-- FIXME: 'forcenames' is an almighty hack! Need a better way of

917-- erasing non-forceable things

938-- erasing non-forceable things

918-- ^^^

939-- ^^^

@@ -1863,7 +1884,7 @@ elabClass info syn doc fc constraints tn ps pDocs ds

1863 constraint

1884 constraint

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

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

1865 let ddecl = PDatadecl tn tty cons

1886 let ddecl = PDatadecl tn tty cons

1866− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

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

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

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

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

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

1869 logLvl 5 $ "Building functions"

1890 logLvl 5 $ "Building functions"

@@ -2059,7 +2080,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2059 let wbTys = map mkTyDecl mtys

2080 let wbTys = map mkTyDecl mtys

2060 let wbVals = map (decorateid (decorate ns iname)) ds'

2081 let wbVals = map (decorateid (decorate ns iname)) ds'

2061 let wb = wbTys ++ wbVals

2082 let wb = wbTys ++ wbVals

2062− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

2083+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

2063 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

2084 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

2064 show (concat (nub wparams))

2085 show (concat (nub wparams))

2065

2086

src/Idris/IBC.hs+19−10

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 69

33+ibcVersion = 70

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -53,6 +53,7 @@ data IBCFile = IBCFile { ver :: Word8,

53 ibc_hdrs :: [(Codegen, String)],

54 ibc_access :: [(Name, Accessibility)],

55 ibc_total :: [(Name, Totality)],

56+ ibc_totcheckfail :: [(FC, String)],

56 ibc_flags :: [(Name, [FnOpt])],

57 ibc_flags :: [(Name, [FnOpt])],

57 ibc_cg :: [(Name, CGInfo)],

58 ibc_cg :: [(Name, CGInfo)],

58 ibc_defs :: [(Name, Def)],

59 ibc_defs :: [(Name, Def)],

@@ -75,7 +76,7 @@ deriving instance Binary IBCFile

75!-}

76!-}

76

77

77initIBC :: IBCFile

78initIBC :: IBCFile

78−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

79+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

79

80

80loadIBC :: FilePath -> Idris ()

81loadIBC :: FilePath -> Idris ()

81loadIBC fp = do imps <- getImported

82loadIBC fp = do imps <- getImported

@@ -234,11 +235,12 @@ ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_

234ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

235ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

235ibc i (IBCFunctionErrorHandler fn a n) f =

236ibc i (IBCFunctionErrorHandler fn a n) f =

236 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

237 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

237−ibc i (IBCMetavar n) f =

238+ibc i (IBCMetavar n) f =

238 case lookup n (idris_metavars i) of

239 case lookup n (idris_metavars i) of

239 Nothing -> return f

240 Nothing -> return f

240 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

241 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

241ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

242ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

243+ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

242

244

243process :: IBCFile -> FilePath -> Idris ()

245process :: IBCFile -> FilePath -> Idris ()

244process i fn

246process i fn

@@ -246,7 +248,7 @@ process i fn

246 ifail "Incorrect ibc version --- please rebuild"

248 ifail "Incorrect ibc version --- please rebuild"

247 | otherwise =

249 | otherwise =

248 do srcok <- runIO $ doesFileExist (sourcefile i)

250 do srcok <- runIO $ doesFileExist (sourcefile i)

249− when srcok $ runIO $ timestampOlder (sourcefile i) fn

251+ when srcok $ timestampOlder (sourcefile i) fn

250 v <- verbose

252 v <- verbose

251 quiet <- getQuiet

253 quiet <- getQuiet

252-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

254-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

@@ -270,6 +272,7 @@ process i fn

270 pPatdefs (ibc_patdefs i)

272 pPatdefs (ibc_patdefs i)

271 pAccess (ibc_access i)

273 pAccess (ibc_access i)

272 pTotal (ibc_total i)

274 pTotal (ibc_total i)

275+ pTotCheckErr (ibc_totcheckfail i)

273 pCG (ibc_cg i)

276 pCG (ibc_cg i)

274 pDocs (ibc_docstrings i)

277 pDocs (ibc_docstrings i)

275 pCoercions (ibc_coercions i)

278 pCoercions (ibc_coercions i)

@@ -283,11 +286,11 @@ process i fn

283 pMetavars (ibc_metavars i)

286 pMetavars (ibc_metavars i)

284 pPostulates (ibc_postulates i)

287 pPostulates (ibc_postulates i)

285

288

286−timestampOlder :: FilePath -> FilePath -> IO ()

289+timestampOlder :: FilePath -> FilePath -> Idris ()

287−timestampOlder src ibc = do srct <- getModificationTime src

290+timestampOlder src ibc = do srct <- runIO $ getModificationTime src

288− ibct <- getModificationTime ibc

291+ ibct <- runIO $ getModificationTime ibc

289 if (srct > ibct)

292 if (srct > ibct)

290− then fail "Needs reloading"

293+ then ifail "Needs reloading"

291 else return ()

294 else return ()

292

295

293pPostulates :: [Name] -> Idris ()

296pPostulates :: [Name] -> Idris ()

@@ -454,6 +457,10 @@ pTotal ds = mapM_ (\ (n, a) ->

454 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

457 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

455 ds

458 ds

456

459

460+pTotCheckErr :: [(FC, String)] -> Idris ()

461+pTotCheckErr es = do ist <- getIState

462+ putIState ist { idris_totcheckfail = idris_totcheckfail ist ++ es }

463+

457pCG :: [(Name, CGInfo)] -> Idris ()

464pCG :: [(Name, CGInfo)] -> Idris ()

458pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

465pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

459

466

@@ -1161,7 +1168,7 @@ instance Binary MetaInformation where

1161 return (DataMI x1)

1168 return (DataMI x1)

1162

1169

1163instance Binary IBCFile where

1170instance Binary IBCFile where

1164− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36)

1171+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

1165 = {-# SCC "putIBCFile" #-}

1172 = {-# SCC "putIBCFile" #-}

1166 do put x1

1173 do put x1

1167 put x2

1174 put x2

@@ -1199,6 +1206,7 @@ instance Binary IBCFile where

1199 put x34

1206 put x34

1200 put x35

1207 put x35

1201 put x36

1208 put x36

1209+ put x37

1202

1210

1203 get

1211 get

1204 = do x1 <- get

1212 = do x1 <- get

@@ -1238,7 +1246,8 @@ instance Binary IBCFile where

1238 x34 <- get

1246 x34 <- get

1239 x35 <- get

1247 x35 <- get

1240 x36 <- get

1248 x36 <- get

1249+ x37 <- get

1241− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36)

1250+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

1242 else return (initIBC { ver = x1 })

1251 else return (initIBC { ver = x1 })

1243

1252

1244instance Binary DataOpt where

1253instance Binary DataOpt where

src/Idris/IdeSlave.hs+29−3

@@ -12,7 +12,7 @@ import Text.Trifecta.Delta

12

13import Idris.Core.TT

14

15−import Control.Applicative

15+import Control.Applicative hiding (Const)

16

17data SExp = SexpList [SExp]

18 | StringAtom String

@@ -84,6 +84,22 @@ maybeProps [] = []

84maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps

85maybeProps ((n, Nothing):ps) = maybeProps ps

86

87+constTy :: Const -> String

88+constTy (I _) = "Int"

89+constTy (BI _) = "Integer"

90+constTy (Fl _) = "Float"

91+constTy (Ch _) = "Char"

92+constTy (Str _) = "String"

93+constTy (B8 _) = "Bits8"

94+constTy (B16 _) = "Bits16"

95+constTy (B32 _) = "Bits32"

96+constTy (B64 _) = "Bits64"

97+constTy (B8V _) = "Bits8x16"

98+constTy (B16V _) = "Bits16x8"

99+constTy (B32V _) = "Bits32x4"

100+constTy (B64V _) = "Bits64x2"

101+constTy _ = "Type"

102+

87instance SExpable OutputAnnotation where

103instance SExpable OutputAnnotation where

88 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

104 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

89 (SymbolAtom "implicit", BoolAtom False)] ++

105 (SymbolAtom "implicit", BoolAtom False)] ++

@@ -92,8 +108,18 @@ instance SExpable OutputAnnotation where

92 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

108 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

93 (SymbolAtom "decor", SymbolAtom "bound"),

109 (SymbolAtom "decor", SymbolAtom "bound"),

94 (SymbolAtom "implicit", BoolAtom imp)]

110 (SymbolAtom "implicit", BoolAtom imp)]

95− toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

111+ toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",

112+ SymbolAtom (if constIsType c then "type" else "data")),

113+ (SymbolAtom "type", StringAtom (constTy c)),

114+ (SymbolAtom "doc-overview", StringAtom (constDocs c)),

115+ (SymbolAtom "name", StringAtom (show c))]

116+ toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),

117+ (SymbolAtom "type", StringAtom ty),

118+ (SymbolAtom "doc-overview", StringAtom doc)]

96− toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]

119+ toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"),

120+ (SymbolAtom "type", StringAtom "Type"),

121+ (SymbolAtom "doc-overview", StringAtom doc)] ++

122+ if not (null name) then [(SymbolAtom "name", StringAtom name)] else []

97 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

123 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

98 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

124 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

99 ((SymbolAtom "filename", StringAtom f),

125 ((SymbolAtom "filename", StringAtom f),

src/Idris/IdrisDoc.hs+8−6

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

5module Idris.IdrisDoc (generateDocs) where

6

7import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),

8− TextFormatting (..), txt, str, nsroot)

8+ TextFormatting (..), txt, str, nsroot, constIsType)

9import Idris.Core.Evaluate (ctxtAlist, Def (..), lookupDefAcc,

10 Accessibility (..), isDConName, isFnName,

11 isTConName)

@@ -455,15 +455,17 @@ genTypeHeader ist (FD n _ args ftype _) = do

455 H.span ! class_ "word" $ do nbsp; ":"; nbsp

456 H.span ! class_ "signature" $ preEscapedToHtml htmlSignature

457

458− where

458+ where

459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names (idris_infixes ist) ftype

460+ signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype

461 names = [ n | (n@(UN n'), _, _, _) <- args,

462 not (T.isPrefixOf (txt "__") n') ]

463

464− decorator AnnConstData str = htmlSpan str "data" str

464+ decorator (AnnConst c) str | constIsType c = htmlSpan str "type" str

465+ | otherwise = htmlSpan str "data" str

465− decorator AnnConstType str = htmlSpan str "type" str

466+ decorator (AnnData _ _) str = htmlSpan str "data" str

466− decorator AnnKeyword str = htmlSpan "" "keyword" str

467+ decorator (AnnType _ _) str = htmlSpan str "type" str

468+ decorator AnnKeyword str = htmlSpan "" "keyword" str

467 decorator (AnnBoundName n i) str | Just t <- M.lookup n docs =

469 decorator (AnnBoundName n i) str | Just t <- M.lookup n docs =

468 let cs = (if i then "implicit " else "") ++ "documented boundvar"

470 let cs = (if i then "implicit " else "") ++ "documented boundvar"

469 in htmlSpan t cs str

471 in htmlSpan t cs str

src/Idris/Interactive.hsnew file+220

@@ -0,0 +1,220 @@

1+module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,

2+ addMissing, makeWith, doProofSearch) where

3+

4+{- Bits and pieces for editing source files interactively, called from

5+ the REPL -}

6+

7+import Idris.Core.TT

8+import Idris.Core.Evaluate

9+import Idris.CaseSplit

10+import Idris.AbsSyntax

11+import Idris.ElabDecls

12+import Idris.Error

13+import Idris.Delaborate

14+import Idris.Output

15+

16+import Util.Pretty

17+import Util.System

18+

19+import System.FilePath

20+import System.Directory

21+import System.IO

22+import Data.Char

23+

24+

25+caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

26+caseSplitAt h fn updatefile l n

27+ = do src <- runIO $ readFile fn

28+ res <- splitOnLine l n fn

29+ iLOG (showSep "\n" (map show res))

30+ let (before, (ap : later)) = splitAt (l-1) (lines src)

31+ res' <- replaceSplits ap res

32+ let new = concat res'

33+ if updatefile

34+ then do let fb = fn ++ "~" -- make a backup!

35+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)

36+ runIO $ copyFile fb fn

37+ else -- do ihputStrLn h (show res)

38+ ihPrintResult h new

39+

40+addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

41+addClauseFrom h fn updatefile l n

42+ = do src <- runIO $ readFile fn

43+ let (before, tyline : later) = splitAt (l-1) (lines src)

44+ let indent = getIndent 0 (show n) tyline

45+ cl <- getClause l n fn

46+ -- add clause before first blank line in 'later'

47+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

48+ if updatefile

49+ then do let fb = fn ++ "~"

50+ runIO $ writeFile fb (unlines (before ++ nonblank) ++

51+ replicate indent ' ' ++

52+ cl ++ "\n" ++

53+ unlines rest)

54+ runIO $ copyFile fb fn

55+ else ihPrintResult h cl

56+ where

57+ getIndent i n [] = 0

58+ getIndent i n xs | take (length n) xs == n = i

59+ getIndent i n (x : xs) = getIndent (i + 1) n xs

60+

61+addProofClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

62+addProofClauseFrom h fn updatefile l n

63+ = do src <- runIO $ readFile fn

64+ let (before, tyline : later) = splitAt (l-1) (lines src)

65+ let indent = getIndent 0 (show n) tyline

66+ cl <- getProofClause l n fn

67+ -- add clause before first blank line in 'later'

68+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

69+ if updatefile

70+ then do let fb = fn ++ "~"

71+ runIO $ writeFile fb (unlines (before ++ nonblank) ++

72+ replicate indent ' ' ++

73+ cl ++ "\n" ++

74+ unlines rest)

75+ runIO $ copyFile fb fn

76+ else ihPrintResult h cl

77+ where

78+ getIndent i n [] = 0

79+ getIndent i n xs | take (length n) xs == n = i

80+ getIndent i n (x : xs) = getIndent (i + 1) n xs

81+

82+addMissing :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

83+addMissing h fn updatefile l n

84+ = do src <- runIO $ readFile fn

85+ let (before, tyline : later) = splitAt (l-1) (lines src)

86+ let indent = getIndent 0 (show n) tyline

87+ i <- getIState

88+ cl <- getInternalApp fn l

89+ let n' = getAppName cl

90+

91+ extras <- case lookupCtxt n' (idris_patdefs i) of

92+ [] -> return ""

93+ [(_, tms)] -> do tms' <- nameMissing tms

94+ showNew (show n ++ "_rhs") 1 indent tms'

95+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

96+ if updatefile

97+ then do let fb = fn ++ "~"

98+ runIO $ writeFile fb (unlines (before ++ nonblank)

99+ ++ extras ++ unlines rest)

100+ runIO $ copyFile fb fn

101+ else ihPrintResult h extras

102+ where showPat = show . stripNS

103+ stripNS tm = mapPT dens tm where

104+ dens (PRef fc n) = PRef fc (nsroot n)

105+ dens t = t

106+

107+ nsroot (NS n _) = nsroot n

108+ nsroot (SN (WhereN _ _ n)) = nsroot n

109+ nsroot n = n

110+

111+ getAppName (PApp _ r _) = getAppName r

112+ getAppName (PRef _ r) = r

113+ getAppName _ = n

114+

115+ showNew nm i ind (tm : tms)

116+ = do (nm', i') <- getUniq nm i

117+ rest <- showNew nm i' ind tms

118+ return (replicate ind ' ' ++

119+ showPat tm ++ " = ?" ++ nm' ++

120+ "\n" ++ rest)

121+ showNew nm i _ [] = return ""

122+

123+ getIndent i n [] = 0

124+ getIndent i n xs | take (length n) xs == n = i

125+ getIndent i n (x : xs) = getIndent (i + 1) n xs

126+

127+

128+makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

129+makeWith h fn updatefile l n

130+ = do src <- runIO $ readFile fn

131+ let (before, tyline : later) = splitAt (l-1) (lines src)

132+ let ind = getIndent tyline

133+ let with = mkWith tyline n

134+ -- add clause before first blank line in 'later',

135+ -- or (TODO) before first line with same indentation as tyline

136+ let (nonblank, rest) = span (\x -> not (all isSpace x) &&

137+ not (ind == getIndent x)) later

138+ if updatefile then

139+ do let fb = fn ++ "~"

140+ runIO $ writeFile fb (unlines (before ++ nonblank)

141+ ++ with ++ "\n" ++

142+ unlines rest)

143+ runIO $ copyFile fb fn

144+ else ihPrintResult h with

145+ where getIndent s = length (takeWhile isSpace s)

146+

147+

148+doProofSearch :: Handle -> FilePath -> Bool -> Bool ->

149+ Int -> Name -> [Name] -> Idris ()

150+doProofSearch h fn updatefile rec l n hints

151+ = do src <- runIO $ readFile fn

152+ let (before, tyline : later) = splitAt (l-1) (lines src)

153+ ctxt <- getContext

154+ mn <- case lookupNames n ctxt of

155+ [x] -> return x

156+ [] -> return n

157+ ns -> ierror (CantResolveAlts (map show ns))

158+ i <- getIState

159+ let (top, envlen, _) = case lookup mn (idris_metavars i) of

160+ Just (t, e, False) -> (t, e, False)

161+ _ -> (Nothing, 0, True)

162+ let fc = fileFC fn

163+ let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))

164+ (ProofSearch rec t hints)]

165+ let def = PClause fc mn (PRef fc mn) [] (body top) []

166+ newmv <- idrisCatch

167+ (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

168+ (tm, ty) <- elabVal toplevel False (PRef fc mn)

169+ ctxt <- getContext

170+ i <- getIState

171+ return . flip displayS "" . renderPretty 1.0 80 $

172+ pprintPTerm defaultPPOption [] [] (idris_infixes i)

173+ (stripNS

174+ (dropCtxt envlen

175+ (delab i (specialise ctxt [] [(mn, 1)] tm)))))

176+ (\e -> return ("?" ++ show n))

177+ if updatefile then

178+ do let fb = fn ++ "~"

179+ runIO $ writeFile fb (unlines before ++

180+ updateMeta False tyline (show n) newmv ++ "\n"

181+ ++ unlines later)

182+ runIO $ copyFile fb fn

183+ else ihPrintResult h newmv

184+ where dropCtxt 0 sc = sc

185+ dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

186+ dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

187+ dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc

188+ dropCtxt _ t = t

189+

190+ stripNS tm = mapPT dens tm where

191+ dens (PRef fc n) = PRef fc (nsroot n)

192+ dens t = t

193+

194+ nsroot (NS n _) = nsroot n

195+ nsroot (SN (WhereN _ _ n)) = nsroot n

196+ nsroot n = n

197+

198+ updateMeta brack ('?':cs) n new

199+ | length cs >= length n

200+ = case splitAt (length n) cs of

201+ (mv, c:cs) ->

202+ if ((isSpace c || c == ')' || c == '}') && mv == n)

203+ then addBracket brack new ++ (c : cs)

204+ else '?' : mv ++ c : updateMeta True cs n new

205+ (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv

206+ updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new

207+ updateMeta brack (c:cs) n new

208+ = c : updateMeta (brack || not (isSpace c)) cs n new

209+ updateMeta brack [] n new = ""

210+

211+ addBracket False new = new

212+ addBracket True new@('(':xs) | last xs == ')' = new

213+ addBracket True new | any isSpace new = '(' : new ++ ")"

214+ | otherwise = new

215+

216+

217+

218+

219+

220+

src/Idris/Output.hs+16−6

@@ -11,8 +11,12 @@ import Idris.IdeSlave

11import Util.Pretty

12import Util.ScreenSize (getScreenWidth)

13

14+import Debug.Trace

15+

14import System.IO (stdout, Handle, hPutStrLn)

16import System.IO (stdout, Handle, hPutStrLn)

15

17

18+import Data.List (nub)

19+

16pshow :: IState -> Err -> String

20pshow :: IState -> Err -> String

17pshow ist err = displayDecorated (consoleDecorate ist) .

21pshow ist err = displayDecorated (consoleDecorate ist) .

18 renderPretty 1.0 80 .

22 renderPretty 1.0 80 .

@@ -88,16 +92,16 @@ ihPrintTermWithType h tm ty = do ist <- getIState

88-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

92-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

89ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

93ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

90ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

94ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

91−ihPrintFunTypes h bnd n overloads = do imp <- impShow

95+ihPrintFunTypes h bnd n overloads = do ist <- getIState

92− ist <- getIState

96+ let ppo = ppOptionIst ist

93 let infixes = idris_infixes ist

97 let infixes = idris_infixes ist

94− let output = vsep (map (uncurry (ppOverload imp infixes)) overloads)

98+ let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

95 case idris_outputmode ist of

99 case idris_outputmode ist of

96 RawOutput -> consoleDisplayAnnotated h output

100 RawOutput -> consoleDisplayAnnotated h output

97 IdeSlave n -> ideSlaveReturnAnnotated n h output

101 IdeSlave n -> ideSlaveReturnAnnotated n h output

98 where fullName n = prettyName True bnd n

102 where fullName n = prettyName True bnd n

99− ppOverload imp infixes n tm =

103+ ppOverload ppo infixes n tm =

100− fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)

104+ fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

101

105

102ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

106ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

103ihRenderResult h d = do ist <- getIState

107ihRenderResult h d = do ist <- getIState

@@ -123,7 +127,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

123 out = displayS . renderPretty 1.0 50 $ renderDocstring o

127 out = displayS . renderPretty 1.0 50 $ renderDocstring o

124 return (out "")

128 return (out "")

125 getTy :: IState -> Name -> String -- fails if name not already extant!

129 getTy :: IState -> Name -> String -- fails if name not already extant!

126− getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist) $

130+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

127 delabTy ist n

131 delabTy ist n

128 in (displayS . renderPretty 1.0 50 $ theTy) ""

132 in (displayS . renderPretty 1.0 50 $ theTy) ""

129fancifyAnnots _ annot = annot

133fancifyAnnots _ annot = annot

@@ -175,3 +179,9 @@ iputGoal g = do i <- getIState

175 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

179 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

176 IdeSlave n -> runIO . putStrLn $

180 IdeSlave n -> runIO . putStrLn $

177 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

181 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

182+

183+-- | Warn about totality problems without failing to compile

184+warnTotality :: Idris ()

185+warnTotality = do ist <- getIState

186+ mapM_ (warn ist) (nub (idris_totcheckfail ist))

187+ where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))

src/Idris/ParseExpr.hs+1

@@ -332,6 +332,7 @@ simpleExpr syn =

332{- |Parses an expression in braces

333@

334Bracketed ::= '(' Bracketed'

335+@

335 -}

336 -}

336bracketed :: SyntaxInfo -> IdrisParser PTerm

337bracketed :: SyntaxInfo -> IdrisParser PTerm

337bracketed syn = do lchar '(' <?> "parenthesized expression"

338bracketed syn = do lchar '(' <?> "parenthesized expression"

src/Idris/Parser.hs+8−5

@@ -47,7 +47,7 @@ import qualified Util.Pretty as P

47import Idris.Core.TT

48import Idris.Core.Evaluate

49

50−import Control.Applicative

50+import Control.Applicative hiding (Const)

51import Control.Monad

52import Control.Monad.Error (throwError, catchError)

53import Control.Monad.State.Strict

@@ -1000,7 +1000,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1000 Right msg ->

1001 fail $ msg)]

1002 <|> do try (lchar '%' *> reserved "name")

1003− ty <- iName []

1003+ ty <- fnName

1004 ns <- sepBy1 name (lchar ',')

1005 return [PDirective (do ty' <- disambiguate ty

1006 mapM_ (addNameHint ty') ns

@@ -1086,6 +1086,10 @@ transform syn = do try (lchar '%' *> reserved "transform")

1086parseExpr :: IState -> String -> Result PTerm

1087parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1088

1089+{- | Parses a constant form input -}

1090+parseConst :: IState -> String -> Result Const

1091+parseConst st = runparser constant st "(input)"

1092+

1089{- | Parses a tactic from input -}

1093{- | Parses a tactic from input -}

1090parseTactic :: IState -> String -> Result PTactic

1094parseTactic :: IState -> String -> Result PTactic

1091parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1095parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

@@ -1224,7 +1228,7 @@ loadSource h lidr f

1224 case fp of

1228 case fp of

1225 LIDR fn -> ifail $ "No ibc for " ++ f

1229 LIDR fn -> ifail $ "No ibc for " ++ f

1226 IDR fn -> ifail $ "No ibc for " ++ f

1230 IDR fn -> ifail $ "No ibc for " ++ f

1227− IBC fn src -> loadIBC fn)

1231+ IBC fn src -> loadIBC fn)

1228 [fn | (fn, _, _) <- imports]

1232 [fn | (fn, _, _) <- imports]

1229 reportParserWarnings

1233 reportParserWarnings

1230

1234

@@ -1248,7 +1252,7 @@ loadSource h lidr f

1248 -- Parsing done, now process declarations

1252 -- Parsing done, now process declarations

1249

1253

1250 let ds = namespaces mname ds'

1254 let ds = namespaces mname ds'

1251− logLvl 3 (show $ showDecls True ds)

1255+ logLvl 3 (show $ showDecls verbosePPOption ds)

1252 i <- getIState

1256 i <- getIState

1253 logLvl 10 (show (toAlist (idris_implicits i)))

1257 logLvl 10 (show (toAlist (idris_implicits i)))

1254 logLvl 3 (show (idris_infixes i))

1258 logLvl 3 (show (idris_infixes i))

@@ -1290,7 +1294,6 @@ loadSource h lidr f

1290 addHides (hide_list i)

1294 addHides (hide_list i)

1291

1295

1292 -- Finally, write an ibc if checking was successful

1296 -- Finally, write an ibc if checking was successful

1293−

1294 ok <- noErrors

1297 ok <- noErrors

1295 when ok $

1298 when ok $

1296 idrisCatch (do writeIBC f ibc; clearIBC)

1299 idrisCatch (do writeIBC f ibc; clearIBC)

src/Idris/Prover.hs+13−12

@@ -110,9 +110,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

110 iputGoal rendered

111

112 where

113− showImplicits = opt_showimp (idris_options ist)

113+ ppo = ppOptionIst ist

114

115− tPretty bnd t = pprintPTerm showImplicits bnd [] (idris_infixes ist) $ delab ist t

115+ tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t

116

117 assumptionNames :: Env -> [Name]

118 assumptionNames = map fst

@@ -122,10 +122,11 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

122 prettyPs bnd ((n@(MN _ r), _) : bs)

123 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

124 prettyPs bnd ((n, Let t v) : bs) =

125− nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

125+ line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

126− tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

126+ align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs

127 prettyPs bnd ((n, b) : bs) =

128+ line <> bindingOf n False <+> colon <+>

128− line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

129+ align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

129

130

130 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

131 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

131 prettyG bnd b = tPretty bnd $ binderTy b

132 prettyG bnd b = tPretty bnd $ binderTy b

@@ -237,16 +238,16 @@ ploop fn d prompt prf e h

237 ctxt' = envCtxt env ctxt

238 ctxt' = envCtxt env ctxt

238 putIState ist { tt_ctxt = ctxt' }

239 putIState ist { tt_ctxt = ctxt' }

239 (tm, ty) <- elabVal toplevel False t

240 (tm, ty) <- elabVal toplevel False t

240− let imp = opt_showimp (idris_options ist)

241+ let ppo = ppOptionIst ist

241 ty' = normaliseC ctxt [] ty

242 ty' = normaliseC ctxt [] ty

242 h = idris_outh ist

243 h = idris_outh ist

243 infixes = idris_infixes ist

244 infixes = idris_infixes ist

244 case tm of

245 case tm of

245 TType _ ->

246 TType _ ->

246− ihPrintTermWithType h (prettyImp imp PType) type1Doc

247+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

247 _ -> let bnd = map (\x -> (fst x, False)) env in

248 _ -> let bnd = map (\x -> (fst x, False)) env in

248− ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))

249+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

249− (pprintPTerm imp bnd [] infixes (delab ist ty))

250+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

250 putIState ist

251 putIState ist

251 return (False, e, False, prf))

252 return (False, e, False, prf))

252 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

253 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -262,10 +263,10 @@ ploop fn d prompt prf e h

262 (tm, ty) <- elabVal toplevel False t

263 (tm, ty) <- elabVal toplevel False t

263 let tm' = force (normaliseAll ctxt' env tm)

264 let tm' = force (normaliseAll ctxt' env tm)

264 ty' = force (normaliseAll ctxt' env ty)

265 ty' = force (normaliseAll ctxt' env ty)

265− imp = opt_showimp (idris_options ist')

266+ ppo = ppOption (idris_options ist')

266 infixes = idris_infixes ist

267 infixes = idris_infixes ist

267− tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')

268+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

268− tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')

269+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

270 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

270 putIState ist

271 putIState ist

271 return (False, e, False, prf))

272 return (False, e, False, prf))

src/Idris/REPL.hs+79−224

@@ -4,6 +4,7 @@

4module Idris.REPL where

5

6import Idris.AbsSyntax

7+import Idris.ASTUtils

7import Idris.Apropos (apropos)

8import Idris.Apropos (apropos)

8import Idris.REPLParser

9import Idris.REPLParser

9import Idris.ElabDecls

10import Idris.ElabDecls

@@ -29,6 +30,7 @@ import Idris.Inliner

29import Idris.CaseSplit

30import Idris.CaseSplit

30import Idris.DeepSeq

31import Idris.DeepSeq

31import Idris.Output

32import Idris.Output

33+import Idris.Interactive

32import Idris.WhoCalls

34import Idris.WhoCalls

33

35

34import Paths_idris

36import Paths_idris

@@ -275,9 +277,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

275 [n] -> Right $ sUN n

277 [n] -> Right $ sUN n

276 (n:ns) -> Right $ sNS (sUN n) ns

278 (n:ns) -> Right $ sNS (sUN n) ns

277runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

279runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

280+ case parseConst orig name of

281+ Success c -> process stdout "(ideslave)" (DocStr (Right c))

282+ Failure _ ->

278− case splitName name of

283+ case splitName name of

279− Left err -> iPrintError err

284+ Left err -> iPrintError err

280− Right n -> process stdout "(ideslave)" (DocStr n)

285+ Right n -> process stdout "(ideslave)" (DocStr (Left n))

281runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

286runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

282 process stdout fn (CaseSplitAt False line (sUN name))

287 process stdout fn (CaseSplitAt False line (sUN name))

283runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

288runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

@@ -312,34 +317,34 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

317runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

313 do ist <- getIState

318 do ist <- getIState

314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

319 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

315− imp <- impShow

320+ let ppo = ppOptionIst ist

316 let mvarTys = map (delabTy ist) mvs

321 let mvarTys = map (delabTy ist) mvs

317 let res = (IdeSlave.SymbolAtom "ok",

322 let res = (IdeSlave.SymbolAtom "ok",

318 zipWith (\ n (prems, concl) -> (n, prems, concl))

323 zipWith (\ n (prems, concl) -> (n, prems, concl))

319 (map (IdeSlave.StringAtom . show) mvs)

324 (map (IdeSlave.StringAtom . show) mvs)

320− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

325+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))

321 runIO . putStrLn $ IdeSlave.convSExp "return" res id

326 runIO . putStrLn $ IdeSlave.convSExp "return" res id

322 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

327 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

323 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

328 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

324 in ((n, t):prems, conc)

329 in ((n, t):prems, conc)

325 getGoal tm = ([], tm)

330 getGoal tm = ([], tm)

326− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

331+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)

327 -> ([(String, String, SpanList OutputAnnotation)],

332 -> ([(String, String, SpanList OutputAnnotation)],

328 (String, SpanList OutputAnnotation))

333 (String, SpanList OutputAnnotation))

329− sexpGoal ist cols imp ns ([], concl) =

334+ sexpGoal ist cols ppo ns ([], concl) =

330 let infixes = idris_infixes ist

335 let infixes = idris_infixes ist

331 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

336 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

332− pprintPTerm imp (zip ns (repeat False)) [] infixes concl

337+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl

333 in ([], concl')

338 in ([], concl')

334− sexpGoal ist cols imp ns ((n, t):ps, concl) =

339+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =

335 let n' = case n of

340 let n' = case n of

336 NS (UN nm) ns -> str nm

341 NS (UN nm) ns -> str nm

337 UN nm | ('_':'_':_) <- str nm -> "_"

342 UN nm | ('_':'_':_) <- str nm -> "_"

338 | otherwise -> str nm

343 | otherwise -> str nm

339 _ -> "_"

344 _ -> "_"

340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

345 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

341− pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t

346+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t

342− rest = sexpGoal ist cols imp (n:ns) (ps, concl)

347+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)

343 in ((n', t', spans) : fst rest, snd rest)

348 in ((n', t', spans) : fst rest, snd rest)

344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

349runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

345 case splitName n of

350 case splitName n of

@@ -581,21 +586,21 @@ process h fn (ExecVal t)

581process h fn (Check (PRef _ n))

586process h fn (Check (PRef _ n))

582 = do ctxt <- getContext

587 = do ctxt <- getContext

583 ist <- getIState

588 ist <- getIState

584− imp <- impShow

589+ let ppo = ppOptionIst ist

585 case lookupNames n ctxt of

590 case lookupNames n ctxt of

586 ts@(t:_) ->

591 ts@(t:_) ->

587 case lookup t (idris_metavars ist) of

592 case lookup t (idris_metavars ist) of

588 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

593 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

589− showMetavarInfo imp ist n i

594+ showMetavarInfo ppo ist n i

590 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

595 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

591 [] -> ihPrintError h $ "No such variable " ++ show n

596 [] -> ihPrintError h $ "No such variable " ++ show n

592 where

597 where

593− showMetavarInfo imp ist n i

598+ showMetavarInfo ppo ist n i

594 = case lookupTy n (tt_ctxt ist) of

599 = case lookupTy n (tt_ctxt ist) of

595− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))

600+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

596− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

601+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

597− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

602+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

598− putTy imp ist i bnd (PPi _ n t sc)

603+ putTy ppo ist i bnd (PPi _ n t sc)

599 = let current = text " " <>

604 = let current = text " " <>

600 (case n of

605 (case n of

601 MN _ _ -> text "_"

606 MN _ _ -> text "_"

@@ -603,21 +608,21 @@ process h fn (Check (PRef _ n))

603 _ -> bindingOf n False) <+>

608 _ -> bindingOf n False) <+>

604 colon <+> align (tPretty bnd ist t) <> line

609 colon <+> align (tPretty bnd ist t) <> line

605 in

610 in

606− current <> putTy imp ist (i-1) ((n,False):bnd) sc

611+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc

607− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

612+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc

608− putGoal imp ist bnd g

613+ putGoal ppo ist bnd g

609 = text "--------------------------------------" <$>

614 = text "--------------------------------------" <$>

610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

615 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

611 align (tPretty bnd ist g)

616 align (tPretty bnd ist g)

612

617

613− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t

618+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

614

619

615

620

616process h fn (Check t)

621process h fn (Check t)

617 = do (tm, ty) <- elabVal toplevel False t

622 = do (tm, ty) <- elabVal toplevel False t

618 ctxt <- getContext

623 ctxt <- getContext

619 ist <- getIState

624 ist <- getIState

620− let imp = opt_showimp (idris_options ist)

625+ let ppo = ppOptionIst ist

621 ty' = normaliseC ctxt [] ty

626 ty' = normaliseC ctxt [] ty

622 case tm of

627 case tm of

623 TType _ ->

628 TType _ ->

@@ -625,7 +630,7 @@ process h fn (Check t)

625 _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

630 _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

626 (prettyIst ist (delab ist ty))

631 (prettyIst ist (delab ist ty))

627

632

628−process h fn (DocStr n)

633+process h fn (DocStr (Left n))

629 = do ist <- getIState

634 = do ist <- getIState

630 case lookupCtxtName n (idris_docstrings ist) of

635 case lookupCtxtName n (idris_docstrings ist) of

631 [] -> iPrintError $ "No documentation for " ++ show n

636 [] -> iPrintError $ "No documentation for " ++ show n

@@ -633,6 +638,11 @@ process h fn (DocStr n)

633 ihRenderResult h (vsep toShow)

638 ihRenderResult h (vsep toShow)

634 where showDoc ist (n, d) = do doc <- getDocs n

639 where showDoc ist (n, d) = do doc <- getDocs n

635 return $ pprintDocs ist doc

640 return $ pprintDocs ist doc

641+

642+process h fn (DocStr (Right c))

643+ = do ist <- getIState

644+ ihRenderResult h $ pprintConstDocs ist c (constDocs c)

645+

636process h fn Universes

646process h fn Universes

637 = do i <- getIState

647 = do i <- getIState

638 let cs = idris_constraints i

648 let cs = idris_constraints i

@@ -664,8 +674,8 @@ process h fn (TotCheck n)

664 [] -> ihPrintError h $ "Unknown operator " ++ show n

674 [] -> ihPrintError h $ "Unknown operator " ++ show n

665 ts -> do ist <- getIState

675 ts -> do ist <- getIState

666 c <- colourise

676 c <- colourise

667− imp <- impShow

677+ let ppo = ppOptionIst ist

668− let showN = showName (Just ist) [] imp c

678+ let showN = showName (Just ist) [] ppo c

669 ihPrintResult h . concat . intersperse "\n" .

679 ihPrintResult h . concat . intersperse "\n" .

670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

680 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

671 ts

681 ts

@@ -689,186 +699,18 @@ process h fn (DebugInfo n)

689 when (not (null cg')) $ do iputStrLn "Call graph:\n"

699 when (not (null cg')) $ do iputStrLn "Call graph:\n"

690 iputStrLn (show cg')

700 iputStrLn (show cg')

691process h fn (Search t) = iPrintError "Not implemented"

701process h fn (Search t) = iPrintError "Not implemented"

692−-- FIXME: There is far too much repetition in the cases below!

693−process h fn (CaseSplitAt updatefile l n)

702+process h fn (CaseSplitAt updatefile l n)

694− = do src <- runIO $ readFile fn

703+ = caseSplitAt h fn updatefile l n

695− res <- splitOnLine l n fn

696− iLOG (showSep "\n" (map show res))

697− let (before, (ap : later)) = splitAt (l-1) (lines src)

698− res' <- replaceSplits ap res

699− let new = concat res'

700− if updatefile

701− then do let fb = fn ++ "~" -- make a backup!

702− runIO $ writeFile fb (unlines before ++ new ++ unlines later)

703− runIO $ copyFile fb fn

704− else -- do ihputStrLn h (show res)

705− ihPrintResult h new

706process h fn (AddClauseFrom updatefile l n)

704process h fn (AddClauseFrom updatefile l n)

707− = do src <- runIO $ readFile fn

708− let (before, tyline : later) = splitAt (l-1) (lines src)

709− let indent = getIndent 0 (show n) tyline

710− cl <- getClause l n fn

711− -- add clause before first blank line in 'later'

712− let (nonblank, rest) = span (not . all isSpace) (tyline:later)

713− if updatefile

705+ = addClauseFrom h fn updatefile l n

714− then do let fb = fn ++ "~"

715− runIO $ writeFile fb (unlines (before ++ nonblank) ++

716− replicate indent ' ' ++

717− cl ++ "\n" ++

718− unlines rest)

719− runIO $ copyFile fb fn

720− else ihPrintResult h cl

721− where

722− getIndent i n [] = 0

723− getIndent i n xs | take (length n) xs == n = i

724− getIndent i n (x : xs) = getIndent (i + 1) n xs

725process h fn (AddProofClauseFrom updatefile l n)

706process h fn (AddProofClauseFrom updatefile l n)

726− = do src <- runIO $ readFile fn

727− let (before, tyline : later) = splitAt (l-1) (lines src)

728− let indent = getIndent 0 (show n) tyline

729− cl <- getProofClause l n fn

730− -- add clause before first blank line in 'later'

731− let (nonblank, rest) = span (not . all isSpace) (tyline:later)

732− if updatefile

707+ = addProofClauseFrom h fn updatefile l n

733− then do let fb = fn ++ "~"

734− runIO $ writeFile fb (unlines (before ++ nonblank) ++

735− replicate indent ' ' ++

736− cl ++ "\n" ++

737− unlines rest)

738− runIO $ copyFile fb fn

739− else ihPrintResult h cl

740− where

741− getIndent i n [] = 0

742− getIndent i n xs | take (length n) xs == n = i

743− getIndent i n (x : xs) = getIndent (i + 1) n xs

744process h fn (AddMissing updatefile l n)

708process h fn (AddMissing updatefile l n)

745− = do src <- runIO $ readFile fn

709+ = addMissing h fn updatefile l n

746− let (before, tyline : later) = splitAt (l-1) (lines src)

747− let indent = getIndent 0 (show n) tyline

748− i <- getIState

749− cl <- getInternalApp fn l

750− let n' = getAppName cl

751−

752− extras <- case lookupCtxt n' (idris_patdefs i) of

753− [] -> return ""

754− [(_, tms)] -> do tms' <- nameMissing tms

755− showNew (show n ++ "_rhs") 1 indent tms'

756− let (nonblank, rest) = span (not . all isSpace) (tyline:later)

757− if updatefile

758− then do let fb = fn ++ "~"

759− runIO $ writeFile fb (unlines (before ++ nonblank)

760− ++ extras ++ unlines rest)

761− runIO $ copyFile fb fn

762− else ihPrintResult h extras

763− where showPat = show . stripNS

764− stripNS tm = mapPT dens tm where

765− dens (PRef fc n) = PRef fc (nsroot n)

766− dens t = t

767−

768− nsroot (NS n _) = nsroot n

769− nsroot (SN (WhereN _ _ n)) = nsroot n

770− nsroot n = n

771−

772− getAppName (PApp _ r _) = getAppName r

773− getAppName (PRef _ r) = r

774− getAppName _ = n

775−

776− showNew nm i ind (tm : tms)

777− = do (nm', i') <- getUniq nm i

778− rest <- showNew nm i' ind tms

779− return (replicate ind ' ' ++

780− showPat tm ++ " = ?" ++ nm' ++

781− "\n" ++ rest)

782− showNew nm i _ [] = return ""

783−

784− getIndent i n [] = 0

785− getIndent i n xs | take (length n) xs == n = i

786− getIndent i n (x : xs) = getIndent (i + 1) n xs

787−

788process h fn (MakeWith updatefile l n)

710process h fn (MakeWith updatefile l n)

789− = do src <- runIO $ readFile fn

711+ = makeWith h fn updatefile l n

790− let (before, tyline : later) = splitAt (l-1) (lines src)

791− let ind = getIndent tyline

792− let with = mkWith tyline n

793− -- add clause before first blank line in 'later',

794− -- or (TODO) before first line with same indentation as tyline

795− let (nonblank, rest) = span (\x -> not (all isSpace x) &&

796− not (ind == getIndent x)) later

797− if updatefile then

798− do let fb = fn ++ "~"

799− runIO $ writeFile fb (unlines (before ++ nonblank)

800− ++ with ++ "\n" ++

801− unlines rest)

802− runIO $ copyFile fb fn

803− else ihPrintResult h with

804− where getIndent s = length (takeWhile isSpace s)

805−

806process h fn (DoProofSearch updatefile rec l n hints)

712process h fn (DoProofSearch updatefile rec l n hints)

807− = do src <- runIO $ readFile fn

713+ = doProofSearch h fn updatefile rec l n hints

808− let (before, tyline : later) = splitAt (l-1) (lines src)

809− ctxt <- getContext

810− mn <- case lookupNames n ctxt of

811− [x] -> return x

812− [] -> return n

813− ns -> ierror (CantResolveAlts (map show ns))

814− i <- getIState

815− let (top, envlen, _) = case lookup mn (idris_metavars i) of

816− Just (t, e, False) -> (t, e, False)

817− _ -> (Nothing, 0, True)

818− let fc = fileFC fn

819− let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))

820− (ProofSearch rec t hints)]

821− let def = PClause fc mn (PRef fc mn) [] (body top) []

822− newmv <- idrisCatch

823− (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

824− (tm, ty) <- elabVal toplevel False (PRef fc mn)

825− ctxt <- getContext

826− i <- getIState

827− return . flip displayS "" . renderPretty 1.0 80 $

828− pprintPTerm False [] [] (idris_infixes i)

829− (stripNS

830− (dropCtxt envlen

831− (delab i (specialise ctxt [] [(mn, 1)] tm)))))

832− (\e -> return ("?" ++ show n))

833− if updatefile then

834− do let fb = fn ++ "~"

835− runIO $ writeFile fb (unlines before ++

836− updateMeta False tyline (show n) newmv ++ "\n"

837− ++ unlines later)

838− runIO $ copyFile fb fn

839− else ihPrintResult h newmv

840− where dropCtxt 0 sc = sc

841− dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

842− dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

843− dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc

844− dropCtxt _ t = t

845−

846− stripNS tm = mapPT dens tm where

847− dens (PRef fc n) = PRef fc (nsroot n)

848− dens t = t

849−

850− nsroot (NS n _) = nsroot n

851− nsroot (SN (WhereN _ _ n)) = nsroot n

852− nsroot n = n

853−

854− updateMeta brack ('?':cs) n new

855− | length cs >= length n

856− = case splitAt (length n) cs of

857− (mv, c:cs) ->

858− if ((isSpace c || c == ')' || c == '}') && mv == n)

859− then addBracket brack new ++ (c : cs)

860− else '?' : mv ++ c : updateMeta True cs n new

861− (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv

862− updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new

863− updateMeta brack (c:cs) n new

864− = c : updateMeta (brack || not (isSpace c)) cs n new

865− updateMeta brack [] n new = ""

866−

867− addBracket False new = new

868− addBracket True new@('(':xs) | last xs == ')' = new

869− addBracket True new | any isSpace new = '(' : new ++ ")"

870− | otherwise = new

871−

872process h fn (Spec t)

714process h fn (Spec t)

873 = do (tm, ty) <- elabVal toplevel False t

715 = do (tm, ty) <- elabVal toplevel False t

874 ctxt <- getContext

716 ctxt <- getContext

@@ -946,6 +788,7 @@ process h fn (Prove n')

946 totcheck (fileFC "(input)", n)

788 totcheck (fileFC "(input)", n)

947 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

789 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

948 mapM_ checkDeclTotality (idris_totcheck i)

790 mapM_ checkDeclTotality (idris_totcheck i)

791+ warnTotality

949

792

950process h fn (HNF t)

793process h fn (HNF t)

951 = do (tm, ty) <- elabVal toplevel False t

794 = do (tm, ty) <- elabVal toplevel False t

@@ -958,23 +801,25 @@ process h fn (TestInline t)

958 ctxt <- getContext

801 ctxt <- getContext

959 ist <- getIState

802 ist <- getIState

960 let tm' = inlineTerm ist tm

803 let tm' = inlineTerm ist tm

961− imp <- impShow

962 c <- colourise

804 c <- colourise

963 iPrintResult (showTm ist (delab ist tm'))

805 iPrintResult (showTm ist (delab ist tm'))

964process h fn Execute

806process h fn Execute

807+ = idrisCatch

965− = do ist <- getIState

808+ (do ist <- getIState

966− (m, _) <- elabVal toplevel False

809+ (m, _) <- elabVal toplevel False

967− (PApp fc

810+ (PApp fc

968− (PRef fc (sUN "run__IO"))

811+ (PRef fc (sUN "run__IO"))

969− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

812+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

970− (tmpn, tmph) <- runIO tempfile

813+ (tmpn, tmph) <- runIO tempfile

971− runIO $ hClose tmph

814+ runIO $ hClose tmph

972− t <- codegen

815+ t <- codegen

973− compile t tmpn m

816+ compile t tmpn m

974− case idris_outputmode ist of

817+ case idris_outputmode ist of

975− RawOutput -> do runIO $ system tmpn

818+ RawOutput -> do runIO $ system tmpn

976− return ()

819+ return ()

820+ IdeSlave n -> runIO . hPutStrLn h $

977− IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n

821+ IdeSlave.convSExp "run-program" tmpn n)

822+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

978 where fc = fileFC "main"

823 where fc = fileFC "main"

979process h fn (Compile codegen f)

824process h fn (Compile codegen f)

980 = do (m, _) <- elabVal toplevel False

825 = do (m, _) <- elabVal toplevel False

@@ -1033,6 +878,8 @@ process h fn (SetOpt AutoSolve) = setAutoSolve True

1033process h fn (UnsetOpt AutoSolve) = setAutoSolve False

878process h fn (UnsetOpt AutoSolve) = setAutoSolve False

1034process h fn (SetOpt NoBanner) = setNoBanner True

879process h fn (SetOpt NoBanner) = setNoBanner True

1035process h fn (UnsetOpt NoBanner) = setNoBanner False

880process h fn (UnsetOpt NoBanner) = setNoBanner False

881+process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

882+process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1036

883

1037process h fn (SetOpt _) = iPrintError "Not a valid option"

884process h fn (SetOpt _) = iPrintError "Not a valid option"

1038process h fn (UnsetOpt _) = iPrintError "Not a valid option"

885process h fn (UnsetOpt _) = iPrintError "Not a valid option"

@@ -1204,13 +1051,18 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

1204 historyFile = hFile

1051 historyFile = hFile

1205 }

1052 }

1206

1053

1207−-- invoke as if from command line

1054+-- | Invoke as if from command line. It is an error if there are unresolved totality problems.

1208idris :: [Opt] -> IO (Maybe IState)

1055idris :: [Opt] -> IO (Maybe IState)

1209−idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit

1056+idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

1210 case res of

1057 case res of

1211 Left err -> do putStrLn $ pshow idrisInit err

1058 Left err -> do putStrLn $ pshow idrisInit err

1212 return Nothing

1059 return Nothing

1213 Right ist -> return (Just ist)

1060 Right ist -> return (Just ist)

1061+ where totalMain = do idrisMain opts

1062+ ist <- getIState

1063+ case idris_totcheckfail ist of

1064+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg

1065+ [] -> return ()

1214

1066

1215

1067

1216loadInputs :: Handle -> [FilePath] -> Idris ()

1068loadInputs :: Handle -> [FilePath] -> Idris ()

@@ -1256,7 +1108,13 @@ loadInputs h inputs

1256 _ -> return ()

1108 _ -> return ()

1257 ist <- getIState

1109 ist <- getIState

1258 putIState (ist { idris_tyinfodata = tidata,

1110 putIState (ist { idris_tyinfodata = tidata,

1259− idris_patdefs = patdefs }))

1111+ idris_patdefs = patdefs })

1112+

1113+ case opt getOutput opts of

1114+ [] -> performUsageAnalysis -- interactive

1115+ _ -> return [] -- batch, will be checked by the compiler

1116+

1117+ return ())

1260 (\e -> do i <- getIState

1118 (\e -> do i <- getIState

1261 case e of

1119 case e of

1262 At f e' -> do setErrSpan f

1120 At f e' -> do setErrSpan f

@@ -1266,8 +1124,8 @@ loadInputs h inputs

1266 ihWarn stdout emptyFC $ pprintErr i e)

1124 ihWarn stdout emptyFC $ pprintErr i e)

1267 where -- load all files, stop if any fail

1125 where -- load all files, stop if any fail

1268 tryLoad :: Bool -> [IFileType] -> Idris ()

1126 tryLoad :: Bool -> [IFileType] -> Idris ()

1269− tryLoad keepstate [] = return ()

1127+ tryLoad keepstate [] = warnTotality >> return ()

1270− tryLoad keepstate (f : fs)

1128+ tryLoad keepstate (f : fs)

1271 = do ist <- getIState

1129 = do ist <- getIState

1272 loadFromIFile h f

1130 loadFromIFile h f

1273 inew <- getIState

1131 inew <- getIState

@@ -1400,10 +1258,7 @@ idrisMain opts =

1400

1258

1401 ok <- noErrors

1259 ok <- noErrors

1402 when ok $ case output of

1260 when ok $ case output of

1403− -- just do the checks

1261+ [] -> return ()

1404− [] -> performUsageAnalysis >> return ()

1405−

1406− -- the compiler will run usage analysis itself

1407 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1262 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1408 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1263 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1409

1264

src/Idris/REPLParser.hs+3−1

@@ -53,7 +53,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

53 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

54 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

55 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

56+ <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))

56− <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr n))

57+ <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))

57 <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))

58 <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))

58 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

59 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

59 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

60 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

@@ -120,6 +121,7 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext

120 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

121 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

121 <|> do discard (P.symbol "autosolve"); return AutoSolve

122 <|> do discard (P.symbol "autosolve"); return AutoSolve

122 <|> do discard (P.symbol "nobanner") ; return NoBanner

123 <|> do discard (P.symbol "nobanner") ; return NoBanner

124+ <|> do discard (P.symbol "warnreach"); return WarnReach

123

125

124codegenOption :: P.IdrisParser Codegen

126codegenOption :: P.IdrisParser Codegen

125codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript

127codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript

test/reg018/expected+1

@@ -1,4 +1,5 @@

1reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

2+reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

2reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

4reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

4reg018d.idr:5:1:Main.pull is not total as there are missing cases

5reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/reg018/run+1

@@ -3,3 +3,4 @@ idris $@ reg018a.idr --check

3idris $@ reg018b.idr --check

4idris $@ reg018c.idr --check

5idris $@ reg018d.idr --check

6+rm *.ibc

test/reg041/expected+1−1

@@ -1,3 +1,3 @@

1Type checking ./ott.idr

2−?prf : (x : Bool) -> (x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)

2+?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

3Z

test/reg043/expectednew file+1

@@ -0,0 +1 @@

1+take : (m : Fin 3) -> Vect 2 Nat -> Vect (finToNat m) Nat

test/reg043/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --nocolour -e "Vect.take {n=2} {a=Nat}"

3+

test/totality001/run+3−3

@@ -1,6 +1,6 @@

1#!/usr/bin/env bash

2−idris $@ test010.idr -o test010

2+idris $@ --check test010.idr

3−idris $@ test010a.idr -o test010

3+idris $@ --check test010a.idr

4−idris $@ test010b.idr -o test010

4+idris $@ --check test010b.idr

5

6rm -f *.ibc

test/totality004/expected+1

@@ -1,2 +1,3 @@

1[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2totality004a.idr:13:1:Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

3+totality004a.idr:24:1:Main.main is possibly not total due to: Main.process

test/totality005/expected−1

@@ -1,2 +1 @@

1−totality005.idr:6:1:Main.fib is possibly not total due to recursive path Main.fib

2[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]

1[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]

test/totality005/totality005.idr+2−1

@@ -2,8 +2,9 @@

2zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c

3zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys

4

5+partial

5fib : Stream Nat

6fib : Stream Nat

6fib = 0 :: zipWithS (+) fib (1 :: fib)

7fib = 0 :: zipWithS (+) fib (1 :: fib)

7

8

8−main : IO ()

9+partial main : IO ()

9main = print (take 15 fib)

10main = print (take 15 fib)

test/totality007/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./Totality.idr

2+Totality.idr:4:1:Totality.foo is not total as there are missing cases

3+Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

test/totality007/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --build totality.ipkg

3+rm -f src/*.ibc

test/totality007/src/Totality.idrnew file+4

@@ -0,0 +1,4 @@

1+module Totality

2+

3+total foo : Nat -> Nat

4+foo Z = Z

test/totality007/totality.ipkgnew file+7

@@ -0,0 +1,7 @@

1+package totality

2+

3+-- totality007

4+-- Test that the package builder doesn't allow totality errors in a build

5+opts = ""

6+sourcedir = src

7+modules = Totality