1c93363 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commit1c93363a4b91e3728f47e2f870413da12f21968f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 5 Jan 2015, 14:13 (12 years ago) parent8f06157 b0257ec

12 files changed+50−14

compare with master

unifiedsplit

.travis.yml+1−1 Makefile+4 README.md+6 idris.cabal+7 src/Idris/Apropos.hs+18−4 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/DeepSeq.hs+1−1 src/Idris/Docstrings.hs+1−1 src/Idris/Elab/Value.hs+1−1 src/Idris/IdeSlave.hs+1−1 src/Idris/Output.hs+1−1 src/Idris/REPL.hs+8−3

.travis.yml+1−1

@@ -20,7 +20,7 @@ before_script:

2020 - tar -xf Idris-dev/dist/idris*.tar.gz

2121 - cd idris*

2222script:

23− - cabal configure -f FFI

23+ - cabal configure -f FFI -f CI

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

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

2626 - if [[ "$TESTS" != "doc" ]]; then cabal register; fi

Makefile+4

@@ -3,6 +3,10 @@

33include config.mk

44-include custom.mk

6+ifdef CI

7+CABALFLAGS += -f CI

8+endif

610install:

711 $(CABAL) install $(CABALFLAGS)

812

README.md+6

@@ -37,6 +37,12 @@ To build with `libffi` by default, create a `custom.mk` file and add the followi

3737

3838The file custom.mk-alldeps is a suitable example.

3939

40+The continues integration builds on travis-ci.org are build using the ghc-flag -Werror. To enable this behaviour locally also, please compile using `make CI=true` or adding the following line into `custom.mk`:

41+

42+`CI = true`

43+

44+If you are only compiling for installing the most current version, you can ommit the CI flag, but please make sure you use it if you want to contribute.

45+

4046## Code Generation

4147

4248Idris has support for external code generators. Supplied with the distribution

idris.cabal+7

@@ -613,6 +613,11 @@ Flag freestanding

613613 Default: False

614614 manual: True

615615

616+Flag CI

617+ Description: Built everything using "-Werror", meant for CI-builds only

618+ Default: False

619+ manual: True

620+

616621Library

617622 hs-source-dirs: src

618623 Exposed-modules:

@@ -791,6 +796,8 @@ Library

791796 if flag(freestanding)

792797 other-modules: Target_idris

793798 cpp-options: -DFREESTANDING

799+ if flag(CI)

800+ ghc-options: -Werror

794801

795802Executable idris

796803 Main-is: Main.hs

src/Idris/Apropos.hs+18−4

@@ -1,12 +1,12 @@

1−module Idris.Apropos where

1+module Idris.Apropos (apropos, aproposModules) where

33import Idris.AbsSyntax

44import Idris.Core.Evaluate (ctxtAlist, Def(..))

55import Idris.Core.TT (Name(..), Type, TT(..), NameType(..), Binder(..), Const(..),

66 lookupCtxtExact, toAlist)

7−import Idris.Docstrings (Docstring, containsText)

7+import Idris.Docstrings (Docstring, DocTerm, containsText)

9−import Data.List (nub)

9+import Data.List (nub, nubBy, intersperse)

1010import qualified Data.Text as T

1111

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

@@ -22,11 +22,25 @@ apropos ist what = let defs = ctxtAlist (tt_ctxt ist)

2222 docs = toAlist (idris_docstrings ist)

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

2424 map fst (isAproposAll parts docs))

25− where isAproposAll [] xs = xs

25+ where isAproposAll [] xs = xs

2626 isAproposAll (what:more) xs = filter (isApropos what)

2727 (isAproposAll more xs)

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

2929

30+-- | Find modules whose names or docstrings contain all the

31+-- space-delimited components of some string.

32+aproposModules :: IState -> T.Text -> [(String, Docstring DocTerm)]

33+aproposModules ist what = let mods = toAlist (idris_moduledocs ist)

34+ found = nubBy (\x y -> fst x == fst y)

35+ (isAproposAll parts mods)

36+ in map unModName found

37+ where isAproposAll [] xs = xs

38+ isAproposAll (what:more) xs = filter (\(n,d) -> isApropos what n || isApropos what d)

39+ (isAproposAll more xs)

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

41+ unModName (NS _ ns, d) = ((concat . intersperse "." . map T.unpack . reverse) ns, d)

42+ unModName (n, d) = ("<<MODULE>>", d)

43+

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

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

3246

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

@@ -1,4 +1,4 @@

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33module Idris.Core.DeepSeq where

src/Idris/DeepSeq.hs+1−1

@@ -1,4 +1,4 @@

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where

src/Idris/Docstrings.hs+1−1

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

11{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

2−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

44-- | Wrapper around Markdown library

55module Idris.Docstrings (

src/Idris/Elab/Value.hs+1−1

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

11{-# LANGUAGE PatternGuards #-}

2−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

55import Idris.AbsSyntax

src/Idris/IdeSlave.hs+1−1

@@ -1,4 +1,4 @@

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

src/Idris/Output.hs+1−1

@@ -1,4 +1,4 @@

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

33module Idris.Output where

src/Idris/REPL.hs+8−3

@@ -5,7 +5,7 @@ module Idris.REPL where

66import Idris.AbsSyntax

77import Idris.ASTUtils

8−import Idris.Apropos (apropos)

8+import Idris.Apropos (apropos, aproposModules)

99import Idris.REPLParser

1010import Idris.ElabDecls

1111import Idris.ElabTerm

@@ -13,7 +13,7 @@ import Idris.Erasure

1313import Idris.Error

1414import Idris.ErrReverse

1515import Idris.Delaborate

16−import Idris.Docstrings (Docstring, overview, renderDocstring)

16+import Idris.Docstrings (Docstring, overview, renderDocstring, renderDocTerm)

1717import Idris.Help

1818import Idris.IdrisDoc

1919import Idris.Prover

@@ -1179,16 +1179,21 @@ process fn (Apropos pkgs a) =

11791179 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

11801180 mapM_ loadPkgIndex pkgs

11811181 ist <- getIState

1182+ let mods = aproposModules ist (T.pack a)

11821183 let names = apropos ist (T.pack a)

11831184 let aproposInfo = [ (n,

11841185 delabTy ist n,

11851186 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

11861187 | n <- sort names, isUN n ]

1187− iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1188+ iRenderResult $ vsep (map (\(m, d) -> text "Module" <+> text m <$>

1189+ ppD ist d <> line) mods) <$>

1190+ vsep (map (prettyDocumentedIst ist) aproposInfo)

11881191 putIState orig

11891192 where isUN (UN _) = True

11901193 isUN (NS n _) = isUN n

11911194 isUN _ = False

1195+ ppD ist = renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) []))

1196+

11921197

11931198process fn (WhoCalls n) =

11941199 do calls <- whoCalls n