da0114d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitda0114d5b86574820e6b6e5d4608ed31363eedff authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 15 Jul 2015, 13:43 (11 years ago) parent6517a95 042c6a5

15 files changed+47−37

compare with master

unifiedsplit

Makefile+4−1 idris.cabal−1 src/Idris/ASTUtils.hs+4−1 src/Idris/Core/ProofState.hs+1−1 src/Idris/Core/TT.hs+27−4 src/Idris/DataOpts.hs+1−1 src/Idris/Directives.hs+1−1 src/Idris/ErrReverse.hs+1−1 src/Idris/IBC.hs−2 src/Idris/Imports.hs+2−1 src/Idris/Inliner.hs+1−1 src/Idris/REPL.hs+3−5 src/Idris/Reflection.hs+1−1 src/Util/ScreenSize.hs+1−1 src/Util/Zlib.hs−15

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

33include config.mk

44-include custom.mk

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

6666user_doc_pdf:

6767 $(MAKE) -C docs latexpdf

6868

69+fast:

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

71+

6972dist/setup-config:

7073 $(CABAL) configure $(CABALFLAGS)

idris.cabal−1

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

868868 Other-modules:

869869 Util.Pretty

870870 , Util.Net

871− , Util.Zlib

872871

873872 , Pkg.PParser

874873

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

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

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

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

760760 let var = P Bound idnm idxt

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

763763

764764

765765equiv :: Raw -> RunTactic

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

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

1818 programs with implicit syntax into fully explicit terms.

1919-}

2020

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

2244

2345-- Work around AMP without CPP

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

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

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

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

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

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

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

2750

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

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

src/Idris/DataOpts.hs+1−1

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

11{-# LANGUAGE PatternGuards #-}

3−module Idris.DataOpts where

3+module Idris.DataOpts(applyOpts) where

55-- Forcing, detagging and collapsing

src/Idris/Directives.hs+1−1

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

2−module Idris.Directives where

2+module Idris.Directives(directiveAction) where

44import Idris.AbsSyntax

55import Idris.ASTUtils

src/Idris/ErrReverse.hs+1−1

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

11{-# LANGUAGE PatternGuards #-}

3−module Idris.ErrReverse where

3+module Idris.ErrReverse(errReverse) where

55import Idris.AbsSyntax

66import Idris.Core.TT

src/Idris/IBC.hs−2

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

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

3737import System.FilePath

3838import System.Directory

39−import Codec.Compression.Zlib (compress)

4039import Codec.Archive.Zip

41−import Util.Zlib (decompressEither)

4240

4341ibcVersion :: Word16

4442ibcVersion = 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

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

45import Data.List (isSuffixOf)

src/Idris/Inliner.hs+1−1

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

11{-# LANGUAGE PatternGuards #-}

3−module Idris.Inliner where

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

55import Idris.Core.TT

66import Idris.AbsSyntax

src/Idris/REPL.hs+3−5

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

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

22 PatternGuards, CPP #-}

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

68import Idris.AbsSyntax

79import Idris.ASTUtils

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

6870

6971import Text.Trifecta.Result(Result(..))

7072

71−-- import RTS.SC

72−-- import RTS.Bytecode

73−-- import RTS.PreC

74−-- import RTS.CodegenC

7573import System.Console.Haskeline as H

7674import System.FilePath

7775import System.Exit

src/Idris/Reflection.hs+1−1

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

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

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

9090reifyApp 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')

9292reifyApp ist t [t']

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

9494reifyApp ist t [t']

src/Util/ScreenSize.hs+1−1

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

11{-# LANGUAGE CPP #-}

2−module Util.ScreenSize where

2+module Util.ScreenSize(getScreenWidth) where

44import Debug.Trace

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