da0114d · Idris-dev · git.iko.soy

Makefile+4−1

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

1−.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test_c test lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs

1+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_c test lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs

2

3include config.mk

4-include custom.mk

@@ -66,5 +66,8 @@ user_doc_html:

66user_doc_pdf:

67 $(MAKE) -C docs latexpdf

68

69+fast:

70+ $(CABAL) install $(CABALFLAGS) --ghc-option=-O0

71+

69dist/setup-config:

72dist/setup-config:

70 $(CABAL) configure $(CABALFLAGS)

73 $(CABAL) configure $(CABALFLAGS)

idris.cabal−1

@@ -868,7 +868,6 @@ Library

868 Other-modules:

869 Util.Pretty

870 , Util.Net

871− , Util.Zlib

872

871

873 , Pkg.PParser

872 , Pkg.PParser

874

873

src/Idris/ASTUtils.hs+4−1

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

1−module Idris.ASTUtils where

1+module Idris.ASTUtils(Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState,

2+ fputState, idris_fixities, ist_callgraph, ist_optimisation,

3+ known_classes, known_terms, opt_detaggable, opt_inaccessible,

4+ opts_idrisCmdline, repl_definitions) where

2

5

3-- This implements just a few basic lens-like concepts to ease state updates.

6-- This implements just a few basic lens-like concepts to ease state updates.

4-- Similar to fclabels in approach, just without the extra dependency.

7-- Similar to fclabels in approach, just without the extra dependency.

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

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

759 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

760 let var = P Bound idnm idxt

761 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

762−induction tm induction ctxt env _ = do fail "Can't do induction here"

762+casetac tm induction ctxt env _ = fail $ "Can't do " ++ (if induction then "induction" else "case analysis") ++ " here"

763

764

765equiv :: Raw -> RunTactic

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

@@ -18,12 +18,35 @@

18 programs with implicit syntax into fully explicit terms.

19-}

20

21−module Idris.Core.TT where

21+module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..),

22+ ConstraintFC(..), DataOpt(..), DataOpts(..), Datatype(..),

23+ Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..),

24+ FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..),

25+ NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..),

26+ Provenance(..), Raw(..), SpecialName(..), TC(..), Term(..),

27+ TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..),

28+ UConstraint(..), UCs(..), UExp(..), Universe(..),

29+ addAlist, addBinder, addDef, allTTNames, arity, bindAll,

30+ bindingOf, bindTyArgs, constDocs, constIsType, deleteDefExact,

31+ discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname,

32+ fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv,

33+ freeNames, getArgTys, getRetTy, implicitable, instantiate,

34+ intTyName, isInjective, isTypeConst, liftPats, lookupCtxt,

35+ lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth,

36+ nextName, noOccurrence, nsroot, occurrences, orderPats,

37+ pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV,

38+ pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget,

39+ safeForgetEnv, score, showCG, showEnv, showEnvDbg, showSep,

40+ sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm,

41+ substV, sUN, tcname, termSmallerThan, tfail, thead, tnull,

42+ toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,

43+ uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP) where

22

44

23-- Work around AMP without CPP

45-- Work around AMP without CPP

24−import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int, Integer, Ordering(..),

46+import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,

47+ Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),

25− Maybe(..), Num(..), Bool(..), Enum(..), Read(..), FilePath, Double,

48+ Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, fst,

26− (&&), (||), ($), (.), div, error, fst, snd, not, mod, read, otherwise)

49+ snd, not, mod, read, otherwise)

27

50

28import Control.Applicative (Applicative (..), Alternative)

51import Control.Applicative (Applicative (..), Alternative)

29import qualified Control.Applicative as A (Alternative (..))

52import qualified Control.Applicative as A (Alternative (..))

src/Idris/DataOpts.hs+1−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2

3−module Idris.DataOpts where

3+module Idris.DataOpts(applyOpts) where

4

5-- Forcing, detagging and collapsing

6

src/Idris/Directives.hs+1−1

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

1

2−module Idris.Directives where

2+module Idris.Directives(directiveAction) where

3

4import Idris.AbsSyntax

5import Idris.ASTUtils

src/Idris/ErrReverse.hs+1−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2

3−module Idris.ErrReverse where

3+module Idris.ErrReverse(errReverse) where

4

5import Idris.AbsSyntax

6import Idris.Core.TT

src/Idris/IBC.hs−2

@@ -36,9 +36,7 @@ import Control.Monad.State.Strict hiding (get, put)

36import qualified Control.Monad.State.Strict as ST

37import System.FilePath

38import System.Directory

39−import Codec.Compression.Zlib (compress)

40import Codec.Archive.Zip

39import Codec.Archive.Zip

41−import Util.Zlib (decompressEither)

42

40

43ibcVersion :: Word16

41ibcVersion :: Word16

44ibcVersion = 114

42ibcVersion = 114

src/Idris/Imports.hs+2−1

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

1−module Idris.Imports where

1+module Idris.Imports(IFileType(..), findImport, findInPath, findPkgIndex,

2+ ibcPathNoFallback, installedPackages, pkgIndex) where

2

3

3import Control.Applicative ((<$>))

4import Control.Applicative ((<$>))

4import Data.List (isSuffixOf)

5import Data.List (isSuffixOf)

src/Idris/Inliner.hs+1−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2

3−module Idris.Inliner where

3+module Idris.Inliner(inlineDef, inlineTerm) where

4

5import Idris.Core.TT

6import Idris.AbsSyntax

src/Idris/REPL.hs+3−5

@@ -1,7 +1,9 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2 PatternGuards, CPP #-}

3

4−module Idris.REPL where

4+module Idris.REPL(getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc,

5+ getPkgREPL, getPkgTest, getPort, idris, idrisMain, loadInputs,

6+ opt, runClient, runMain, ver) where

5

7

6import Idris.AbsSyntax

8import Idris.AbsSyntax

7import Idris.ASTUtils

9import Idris.ASTUtils

@@ -68,10 +70,6 @@ import qualified Data.Text as T

68

70

69import Text.Trifecta.Result(Result(..))

71import Text.Trifecta.Result(Result(..))

70

72

71−-- import RTS.SC

72−-- import RTS.Bytecode

73−-- import RTS.PreC

74−-- import RTS.CodegenC

75import System.Console.Haskeline as H

73import System.Console.Haskeline as H

76import System.FilePath

74import System.FilePath

77import System.Exit

75import System.Exit

src/Idris/Reflection.hs+1−1

@@ -88,7 +88,7 @@ reifyApp ist t [Constant (Str n), x]

88 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

89reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

90reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

91−reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')

91+reifyApp ist t [t'] | t == reflm "Case" = liftM (CaseTac . delab ist) (reifyTT t')

92reifyApp ist t [t']

93 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

94reifyApp ist t [t']

src/Util/ScreenSize.hs+1−1

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

1{-# LANGUAGE CPP #-}

2−module Util.ScreenSize where

2+module Util.ScreenSize(getScreenWidth) where

3

4import Debug.Trace

5

src/Util/Zlib.hsdeleted−15

@@ -1,15 +0,0 @@

1−module Util.Zlib (decompressEither) where

2−

3−-- From http://stackoverflow.com/questions/10043102/how-to-catch-the-decompress-ioerror/10045963#10045963

4−import Codec.Compression.Zlib.Internal

5−import Data.ByteString.Lazy (ByteString, fromChunks)

6−import Control.Arrow (right)

7−

8−decompressEither :: ByteString -> Either (DecompressError, String) ByteString

9−decompressEither = finalise

10− . foldDecompressStream cons nil err

11− . decompressWithErrors zlibFormat defaultDecompressParams

12− where err errorCode errorString = Left (errorCode, errorString)

13− nil = Right []

14− cons chunk = right (chunk :)

15− finalise = right fromChunks