0896073 · Idris-dev · git.iko.soy

src/IRTS/BCImp.hs+7−3

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

1+{-|

2+Module : IRTS.BCImp

3+Description : Bytecode for a register/variable based VM (e.g. for generating code in an imperative language where we let the language deal with GC)

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module IRTS.BCImp where

29

3−-- Bytecode for a register/variable based VM (e.g. for generating code in an

4−-- imperative language where we let the language deal with GC)

5−

610import IRTS.Lang

711import IRTS.Simplified

812import Idris.Core.TT

src/IRTS/Bytecode.hs+37−35

@@ -1,15 +1,11 @@

1−module IRTS.Bytecode where

1+{-|

2+Module : IRTS.Bytecode

3+Description : Bytecode for a stack based VM (e.g. for generating C code with an accurate hand written GC)

24

3−-- Bytecode for a stack based VM (e.g. for generating C code with an accurate

4−-- hand written GC)

5+Copyright :

6+License : BSD3

7+Maintainer : The Idris Community.

58

6−import IRTS.Lang

7−import IRTS.Simplified

8−import IRTS.Defunctionalise

9−import Idris.Core.TT

10−import Data.Maybe

11−

12−{- We have:

139

1410BASE: Current stack frame's base

1511TOP: Top of stack

@@ -22,27 +18,35 @@ RVal is a register in which computed values (essentially, what a function

2218returns) are stored.

2319

2420-}

21+module IRTS.Bytecode where

22+

23+

24+import IRTS.Lang

25+import IRTS.Simplified

26+import IRTS.Defunctionalise

27+import Idris.Core.TT

28+import Data.Maybe

2529

2630data Reg = RVal | L Int | T Int | Tmp

2731 deriving (Show, Eq)

2832

29−data BC =

30− -- reg1 = reg2

33+data BC =

34+ -- | reg1 = reg2

3135 ASSIGN Reg Reg

3236

33− -- reg = const

37+ -- | reg = const

3438 | ASSIGNCONST Reg Const

3539

36− -- reg1 = reg2 (same as assign, it seems)

40+ -- | reg1 = reg2 (same as assign, it seems)

3741 | UPDATE Reg Reg

3842

39− -- reg = constructor, where constructor consists of a tag and

43+ -- | reg = constructor, where constructor consists of a tag and

4044 -- values from registers, e.g. (cons tag args)

4145 -- the 'Maybe Reg', if set, is a register which can be overwritten

4246 -- (i.e. safe for mutable update), though this can be ignored

4347 | MKCON Reg (Maybe Reg) Int [Reg]

4448

45− -- Matching on value of reg: usually (but not always) there are

49+ -- | Matching on value of reg: usually (but not always) there are

4650 -- constructors, hence "Int" for patterns (that's a tag on which

4751 -- we should match), and the following [BC] is just a list of

4852 -- instructions for the corresponding case. The last argument is

@@ -53,57 +57,57 @@ data BC =

5357 | CASE Bool

5458 Reg [(Int, [BC])] (Maybe [BC])

5559

56− -- get a value from register, which should be a constructor, and

60+ -- | get a value from register, which should be a constructor, and

5761 -- put its arguments into the stack, starting from (base + int1)

5862 -- and onwards; second Int provides arity

5963 | PROJECT Reg Int Int

6064

61− -- probably not used

65+ -- | probably not used

6266 | PROJECTINTO Reg Reg Int -- project argument from one reg into another

6367

64− -- same as CASE, but there's an exact value (not constructor) in reg

68+ -- | same as CASE, but there's an exact value (not constructor) in reg

6569 | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])

6670

67− -- just call a function, passing MYOLDBASE (see below) to it

71+ -- | just call a function, passing MYOLDBASE (see below) to it

6872 | CALL Name

6973

70− -- same, perhaps exists just for TCO

74+ -- | same, perhaps exists just for TCO

7175 | TAILCALL Name

7276

73− -- set reg to (apply string args),

77+ -- | set reg to (apply string args),

7478 | FOREIGNCALL Reg FDesc FDesc [(FDesc, Reg)]

7579

76− -- move this number of elements from TOP to BASE

80+ -- | move this number of elements from TOP to BASE

7781 | SLIDE Int

7882

79− -- set BASE = OLDBASE

83+ -- | set BASE = OLDBASE

8084 | REBASE

8185

82− -- reserve n more stack items (i.e. check there's space, grow if

86+ -- | reserve n more stack items (i.e. check there's space, grow if

8387 -- necessary)

8488 | RESERVE Int

8589

86− -- move the top of stack up

90+ -- | move the top of stack up

8791 | ADDTOP Int

8892

89− -- set TOP = BASE + n

93+ -- | set TOP = BASE + n

9094 | TOPBASE Int

9195

92− -- set BASE = TOP + n

96+ -- | set BASE = TOP + n

9397 | BASETOP Int

9498

95− -- set MYOLDBASE = BASE, where MYOLDBASE is a function-local

99+ -- | set MYOLDBASE = BASE, where MYOLDBASE is a function-local

96100 -- variable, set to OLDBASE by default, and passed on function

97101 -- call to called functions as their OLDBASE

98102 | STOREOLD

99103

100− -- reg = apply primitive_function args

104+ -- | reg = apply primitive_function args

101105 | OP Reg PrimFn [Reg]

102106

103− -- clear reg

107+ -- | clear reg

104108 | NULL Reg

105109

106− -- throw an error

110+ -- | throw an error

107111 | ERROR String

108112 deriving Show

109113

@@ -138,7 +142,7 @@ bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

138142bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]

139143 ++ clean r

140144-- bc reg (SUpdate x sc) r = bc reg sc r -- can't update, just do it

141−bc reg (SCon atloc i _ vs) r

145+bc reg (SCon atloc i _ vs) r

142146 = MKCON reg (getAllocLoc atloc) i (map getL vs) : clean r

143147 where getL (Loc x) = L x

144148 getAllocLoc (Just (Loc x)) = Just (L x)

@@ -184,5 +188,3 @@ constAlt l reg r _ = Nothing

184188defaultAlt reg [] r = Nothing

185189defaultAlt reg (SDefaultCase e : _) r = Just (bc reg e r)

186190defaultAlt reg (_ : xs) r = defaultAlt reg xs r

187−

188−

src/IRTS/CodegenC.hs+18−11

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.CodegenC

3+Description : The default code generator for Idris, generating C code.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module IRTS.CodegenC (codegenC) where

29

310import Idris.AbsSyntax

@@ -41,17 +48,17 @@ codegenC ci = do codegenC' (simpleDecls ci)

4148 where mkLib l = "-l" ++ l

4249 incdir i = "-I" ++ i

4350

44−codegenC' :: [(Name, SDecl)] ->

45− String -> -- output file name

46− OutputType -> -- generate executable if True, only .o if False

47− [FilePath] -> -- include files

48− [String] -> -- extra object files

49− [String] -> -- extra compiler flags (libraries)

50− [String] -> -- extra compiler flags (anything)

51− [ExportIFace] ->

52− Bool -> -- interfaces too (so make a .o instead)

53− DbgLevel ->

54− IO ()

51+codegenC' :: [(Name, SDecl)]

52+ -> String -- ^ output file name

53+ -> OutputType -- ^ generate executable if True, only .o if False

54+ -> [FilePath] -- ^ include files

55+ -> [String] -- ^ extra object files

56+ -> [String] -- ^ extra compiler flags (libraries)

57+ -> [String] -- ^ extra compiler flags (anything)

58+ -> [ExportIFace]

59+ -> Bool -- ^ interfaces too (so make a .o instead)

60+ -> DbgLevel

61+ -> IO ()

5562codegenC' defs out exec incs objs libs flags exports iface dbg

5663 = do -- print defs

5764 let bc = map toBC defs

src/IRTS/CodegenCommon.hs+29−19

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.CodegenCommon

3+Description : Common data structures required for all code generators.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module IRTS.CodegenCommon where

29

310import Idris.Core.TT

@@ -7,25 +14,28 @@ import IRTS.Defunctionalise

714data DbgLevel = NONE | DEBUG | TRACE deriving Eq

815data OutputType = Raw | Object | Executable deriving (Eq, Show)

916

10−-- Everything which might be needed in a code generator - a CG can choose which

11−-- level of Decls to generate code from (simplified, defunctionalised or merely

12−-- lambda lifted) and has access to the list of object files, libraries, etc.

17+-- | Everything which might be needed in a code generator.

18+--

19+-- A CG can choose which level of Decls to generate code from

20+-- (simplified, defunctionalised or merely lambda lifted) and has

21+-- access to the list of object files, libraries, etc.

1322

14−data CodegenInfo = CodegenInfo { outputFile :: String,

15− outputType :: OutputType,

16− targetTriple :: String,

17− targetCPU :: String,

18− includes :: [FilePath],

19− importDirs :: [FilePath],

20− compileObjs :: [String],

21− compileLibs :: [String],

22− compilerFlags :: [String],

23− debugLevel :: DbgLevel,

24− simpleDecls :: [(Name, SDecl)],

25− defunDecls :: [(Name, DDecl)],

26− liftDecls :: [(Name, LDecl)],

27− interfaces :: Bool,

28− exportDecls :: [ExportIFace]

29− }

23+data CodegenInfo = CodegenInfo {

24+ outputFile :: String

25+ , outputType :: OutputType

26+ , targetTriple :: String

27+ , targetCPU :: String

28+ , includes :: [FilePath]

29+ , importDirs :: [FilePath]

30+ , compileObjs :: [String]

31+ , compileLibs :: [String]

32+ , compilerFlags :: [String]

33+ , debugLevel :: DbgLevel

34+ , simpleDecls :: [(Name, SDecl)]

35+ , defunDecls :: [(Name, DDecl)]

36+ , liftDecls :: [(Name, LDecl)]

37+ , interfaces :: Bool

38+ , exportDecls :: [ExportIFace]

39+ }

3040

3141type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/CodegenJavaScript.hs+11−1

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

1+{-|

2+Module : IRTS.CodegenJavaScript

3+Description : The JavaScript code generator.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29{-# LANGUAGE OverloadedStrings #-}

3−module IRTS.CodegenJavaScript (codegenJavaScript, codegenNode, JSTarget(..)) where

10+module IRTS.CodegenJavaScript (codegenJavaScript

11+ , codegenNode

12+ , JSTarget(..)

13+ ) where

414

515import IRTS.JavaScript.AST

616

src/IRTS/Compiler.hs+16−7

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.Compiler

3+Description : Coordinates the compilation process.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}

29

310module IRTS.Compiler(compile, generate) where

@@ -32,13 +39,15 @@ import Prelude hiding (id, (.))

3239

3340import Control.Applicative

3441import Control.Monad.State

35−import Data.Maybe

36−import Data.List

37−import Data.Ord

38−import Data.IntSet (IntSet)

39−import qualified Data.IntSet as IS

40−import qualified Data.Map as M

41−import qualified Data.Set as S

42+

43+import Data.Maybe

44+import Data.List

45+import Data.Ord

46+import Data.IntSet (IntSet)

47+import qualified Data.IntSet as IS

48+import qualified Data.Map as M

49+import qualified Data.Set as S

50+

4251import System.Process

4352import System.IO

4453import System.Exit

src/IRTS/Defunctionalise.hs+31−26

@@ -1,7 +1,28 @@

1+{-|

2+Module : IRTS.Defunctionalise

3+Description : Defunctionalise Idris' IR.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+To defunctionalise:

9+

10+1. Create a data constructor for each function

11+2. Create a data constructor for each underapplication of a function

12+3. Convert underapplications to their corresponding constructors

13+4. Create an EVAL function which calls the appropriate function for data constructors

14+ created as part of step 1

15+5. Create an APPLY function which adds an argument to each underapplication (or calls

16+ APPLY again for an exact application)

17+6. Wrap overapplications in chains of APPLY

18+7. Wrap unknown applications (i.e. applications of local variables) in chains of APPLY

19+8. Add explicit EVAL to case, primitives, and foreign calls

20+

21+-}

122{-# LANGUAGE PatternGuards #-}

2−

3−module IRTS.Defunctionalise(module IRTS.Defunctionalise,

4− module IRTS.Lang) where

23+module IRTS.Defunctionalise(module IRTS.Defunctionalise

24+ , module IRTS.Lang

25+ ) where

526

627import IRTS.Lang

728import Idris.Core.TT

@@ -61,19 +82,6 @@ getFn xs = mapMaybe fnData xs

6182 where fnData (n, LFun _ _ args _) = Just (n, length args)

6283 fnData _ = Nothing

6384

64−-- To defunctionalise:

65−--

66−-- 1 Create a data constructor for each function

67−-- 2 Create a data constructor for each underapplication of a function

68−-- 3 Convert underapplications to their corresponding constructors

69−-- 4 Create an EVAL function which calls the appropriate function for data constructors

70−-- created as part of step 1

71−-- 5 Create an APPLY function which adds an argument to each underapplication (or calls

72−-- APPLY again for an exact application)

73−-- 6 Wrap overapplications in chains of APPLY

74−-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY

75−-- 8 Add explicit EVAL to case, primitives, and foreign calls

76−

7785addApps :: LDefs -> (Name, LDecl) -> State ([Name], [(Name, Int)]) (Name, DDecl)

7886addApps defs o@(n, LConstructor _ t a)

7987 = return (n, DConstructor n t a)

@@ -111,7 +119,7 @@ addApps defs (n, LFun _ _ args e)

111119 alts' <- mapM (aaAlt env) alts

112120 return $ DCase up e' alts'

113121 aa env (LConst c) = return $ DConst c

114− aa env (LForeign t n args)

122+ aa env (LForeign t n args)

115123 = do args' <- mapM (aaF env) args

116124 return $ DForeign t n args'

117125 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)

@@ -133,7 +141,7 @@ addApps defs (n, LFun _ _ args e)

133141 = return $ DApp tc n args

134142 | length args < ar

135143 = do (ens, ans) <- get

136− let alln = map (\x -> (n, x)) [length args .. ar]

144+ let alln = map (\x -> (n, x)) [length args .. ar]

137145 put (ens, alln ++ ans)

138146 return $ DApp tc (mkUnderCon n (ar - length args)) args

139147 | length args > ar

@@ -146,14 +154,14 @@ addApps defs (n, LFun _ _ args e)

146154 return $ DApp False (mkFnCon n) args

147155 | length args < ar

148156 = do (ens, ans) <- get

149− let alln = map (\x -> (n, x)) [length args .. ar]

157+ let alln = map (\x -> (n, x)) [length args .. ar]

150158 put (ens, alln ++ ans)

151159 return $ DApp False (mkUnderCon n (ar - length args)) args

152160 | length args > ar

153161 = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)

154162

155163 chainAPPLY f [] = f

156−-- chainAPPLY f (a : b : as)

164+-- chainAPPLY f (a : b : as)

157165-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as

158166 chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as

159167

@@ -223,7 +231,7 @@ mkApplyCase fname n ar

223231 (DApp False (mkUnderCon fname (ar - (n + 1)))

224232 (map (DV . Glob) (take n (genArgs 0) ++

225233 [sMN 0 "arg"])))))

226− :

234+ :

227235 if (ar - (n + 2) >=0 )

228236 then (nm, n, Apply2Case (DConCase (-1) nm (take n (genArgs 0))

229237 (DApp False (mkUnderCon fname (ar - (n + 2)))

@@ -263,7 +271,7 @@ mkApply2 xs = (sMN 0 "APPLY2", DFun (sMN 0 "APPLY2") [sMN 0 "fn", sMN 0 "arg0",

263271 mkBigCase (sMN 0 "APPLY") 256

264272 (DV (Glob (sMN 0 "fn")))

265273 (cases ++

266− [DDefaultCase

274+ [DDefaultCase

267275 (DApp False (sMN 0 "APPLY")

268276 [DApp False (sMN 0 "APPLY")

269277 [DV (Glob (sMN 0 "fn")),

@@ -320,9 +328,8 @@ instance Show DExp where

320328 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e

321329 showAlt env (DDefaultCase e) = "_ => " ++ show' env e

322330

323−-- Divide up a large case expression so that each has a maximum of

331+-- | Divide up a large case expression so that each has a maximum of

324332-- 'max' branches

325−

326333mkBigCase cn max arg branches

327334 | length branches <= max = DChkCase arg branches

328335 | otherwise = -- DChkCase arg branches -- until I think of something...

@@ -368,5 +375,3 @@ dumpDefuns ds = showSep "\n" $ map showDef (toAlist ds)

368375 = show fn ++ "(" ++ showSep ", " (map show args) ++ ") = \n\t" ++

369376 show exp ++ "\n"

370377 showDef (x, DConstructor n t a) = "Constructor " ++ show n ++ " " ++ show t

371−

372−

src/IRTS/DumpBC.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.DumpBC

3+Description : Serialise Idris to its IBC format.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module IRTS.DumpBC where

29

310import IRTS.Lang

src/IRTS/Exports.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.Exports

3+Description : Deal with external things.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module IRTS.Exports(findExports, getExpNames) where

310

src/IRTS/Inliner.hs+7−1

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.Inliner

3+Description : Inline expressions.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module IRTS.Inliner where

29

310import Idris.Core.TT

@@ -19,4 +26,3 @@ inl ds d = d

1926evalD _ e = ev e

2027 where

2128 ev e = Just e

22−

src/IRTS/JavaScript/AST.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.JavaScript.AST

3+Description : Data structures and functions used with the JavaScript codegen.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29{-# LANGUAGE OverloadedStrings #-}

310module IRTS.JavaScript.AST where

src/IRTS/Lang.hs+17−10

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.Lang

3+Description : Internal representation of Idris' constructs.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards, DeriveFunctor #-}

29

310module IRTS.Lang where

@@ -19,19 +26,19 @@ data LVar = Loc Int | Glob Name

1926-- ASSUMPTION: All variable bindings have unique names here

2027-- Constructors commented as lifted are not present in the LIR provided to the different backends.

2128data LExp = LV LVar

22− | LApp Bool LExp [LExp] -- True = tail call

23− | LLazyApp Name [LExp] -- True = tail call

24− | LLazyExp LExp -- lifted out before compiling

25− | LForce LExp -- make sure Exp is evaluted

26− | LLet Name LExp LExp -- name just for pretty printing

27− | LLam [Name] LExp -- lambda, lifted out before compiling

28− | LProj LExp Int -- projection

29− | LCon (Maybe LVar) -- Location to reallocate, if available

29+ | LApp Bool LExp [LExp] -- True = tail call

30+ | LLazyApp Name [LExp] -- True = tail call

31+ | LLazyExp LExp -- lifted out before compiling

32+ | LForce LExp -- make sure Exp is evaluted

33+ | LLet Name LExp LExp -- name just for pretty printing

34+ | LLam [Name] LExp -- lambda, lifted out before compiling

35+ | LProj LExp Int -- projection

36+ | LCon (Maybe LVar) -- Location to reallocate, if available

3037 Int Name [LExp]

3138 | LCase CaseType LExp [LAlt]

3239 | LConst Const

33− | LForeign FDesc -- Function descriptor (usually name as string)

34− FDesc -- Return type descriptor

40+ | LForeign FDesc -- Function descriptor (usually name as string)

41+ FDesc -- Return type descriptor

3542 [(FDesc, LExp)] -- first LExp is the FFI type description

3643 | LOp PrimFn [LExp]

3744 | LNothing

src/IRTS/LangOpts.hs+17−9

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.LangOpts

3+Description : Transformations to apply to Idris' IR.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards, DeriveFunctor #-}

29

310module IRTS.LangOpts where

@@ -20,17 +27,19 @@ nextN = do i <- get

2027 put (i + 1)

2128 return $ sMN i "in"

2229

23−-- Inline inside a declaration. Variables are still Name at this stage.

24−-- Need to preserve uniqueness of variable names in the resulting definition,

25−-- so invent a new name for every variable we encounter

30+-- | Inline inside a declaration.

31+--

32+-- Variables are still Name at this stage. Need to preserve

33+-- uniqueness of variable names in the resulting definition, so invent

34+-- a new name for every variable we encounter

2635doInline :: LDefs -> LDecl -> LDecl

2736doInline defs d@(LConstructor _ _ _) = d

28−doInline defs (LFun opts topn args exp)

37+doInline defs (LFun opts topn args exp)

2938 = let res = evalState (inlineWith [topn] (map (\n -> (n, LV (Glob n))) args) exp) 0 in

3039 LFun opts topn args res

3140 where

3241 inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp

33− inlineWith done env var@(LV (Glob n))

42+ inlineWith done env var@(LV (Glob n))

3443 = case lookup n env of

3544 Just t -> return t

3645 Nothing -> return var

@@ -39,7 +48,7 @@ doInline defs (LFun opts topn args exp)

3948 inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e

4049 -- Extend the environment for Let and Lam so that bound names aren't

4150 -- expanded with any top level argument definitions they shadow

42− inlineWith done env (LLet n val sc)

51+ inlineWith done env (LLet n val sc)

4352 = do n' <- nextN

4453 LLet n' <$> inlineWith done env val <*>

4554 inlineWith done ((n, LV (Glob n')) : env) sc

@@ -51,7 +60,7 @@ doInline defs (LFun opts topn args exp)

5160 inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i

5261 inlineWith done env (LCon loc i n es)

5362 = LCon loc i n <$> mapM (inlineWith done env) es

54− inlineWith done env (LCase ty e alts)

63+ inlineWith done env (LCase ty e alts)

5564 = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts

5665 inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es

5766 -- the interesting case!

@@ -72,8 +81,7 @@ doInline defs (LFun opts topn args exp)

7281 inlineWithAlt done env (LConCase i n es rhs)

7382 = do ns' <- mapM (\n -> do n' <- nextN

7483 return (n, n')) es

75− LConCase i n (map snd ns') <$>

84+ LConCase i n (map snd ns') <$>

7685 inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs

7786 inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e

7887 inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e

79−

src/IRTS/Portable.hs+7−1

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

1+{-|

2+Module : IRTS.Portable

3+Description : Serialise Idris' IR to JSON.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE OverloadedStrings #-}

2−

39module IRTS.Portable (writePortable) where

410

511import Data.Aeson

src/IRTS/Simplified.hs+7−4

@@ -1,3 +1,10 @@

1+{-|

2+Module : IRTS.Simplified

3+Description : Simplified expressions, where functions/constructors can only be applied to variables.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where

29

310import IRTS.Defunctionalise

@@ -9,9 +16,6 @@ import Control.Monad.State

916

1017import Debug.Trace

1118

12−-- Simplified expressions, where functions/constructors can only be applied

13−-- to variables

14−

1519data SExp = SV LVar

1620 | SApp Bool Name [LVar]

1721 | SLet LVar SExp SExp

@@ -231,4 +235,3 @@ scopecheck fn ctxt envTop tm = sc envTop tm where

231235 return (SConstCase c e')

232236 scalt env (SDefaultCase e) = do e' <- sc env e

233237 return (SDefaultCase e')

234−

src/IRTS/System.hs+17−2

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

1+{-|

2+Module : IRTS.System

3+Description : Utilities for interacting with the System.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE CPP #-}

2−module IRTS.System(getDataFileName, getDataDir, getTargetDir,getCC,getLibFlags,getIdrisLibDir,

3− getIncFlags, getEnvFlags, version) where

9+module IRTS.System( getDataFileName

10+ , getDataDir

11+ , getTargetDir

12+ , getCC

13+ , getLibFlags

14+ , getIdrisLibDir

15+ , getIncFlags

16+ , getEnvFlags

17+ , version

18+ ) where

419

520import Data.List.Split

621

src/Idris/ASTUtils.hs+45−35

@@ -1,38 +1,48 @@

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

5−

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

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

8−--

9−-- We don't include an explicit export list

10−-- because everything here is meant to be exported.

11−--

12−-- Short synopsis:

13−-- ---------------

14−--

15−-- f :: Idris ()

16−-- f = do

17−-- -- these two steps:

18−-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)

19−-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)

20−--

21−-- -- are equivalent to:

22−-- fmodifyState (opt_detaggable . ist_optimisation typeName) not

23−--

24−-- -- of course, the long accessor can be put in a variable;

25−-- -- everything is first-class

26−-- let detag n = opt_detaggable . ist_optimisation n

27−-- fputState (detag n1) True

28−-- fputState (detag n2) False

29−--

30−-- -- Note that all these operations handle missing items consistently

31−-- -- and transparently, as prescribed by the default values included

32−-- -- in the definitions of the ist_* functions.

33−-- --

34−-- -- Especially, it's no longer necessary to have initial values of

35−-- -- data structures copied (possibly inconsistently) all over the compiler.

1+{-|

2+Module : Idris.ASTUtils

3+Description : This implements just a few basic lens-like concepts to ease state updates. Similar to fclabels in approach, just without the extra dependency.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

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

9+Similar to fclabels in approach, just without the extra dependency.

10+

11+We don't include an explicit export list

12+because everything here is meant to be exported.

13+

14+Short synopsis:

15+---------------

16+@

17+f :: Idris ()

18+f = do

19+ -- these two steps:

20+ detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)

21+ fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)

22+

23+ -- are equivalent to:

24+ fmodifyState (opt_detaggable . ist_optimisation typeName) not

25+

26+ -- of course, the long accessor can be put in a variable;

27+ -- everything is first-class

28+ let detag n = opt_detaggable . ist_optimisation n

29+ fputState (detag n1) True

30+ fputState (detag n2) False

31+

32+ -- Note that all these operations handle missing items consistently

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

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

35+ --

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

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

38+@

39+-}

40+module Idris.ASTUtils(

41+ Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState

42+ , fputState, idris_fixities, ist_callgraph, ist_optimisation

43+ , known_classes, known_terms, opt_detaggable, opt_inaccessible

44+ , opts_idrisCmdline, repl_definitions

45+ ) where

3646

3747import Control.Category

3848import Control.Applicative

src/Idris/AbsSyntax.hs+11−1

@@ -1,7 +1,17 @@

1+{-|

2+Module : Idris.AbsSyntax

3+Description : Provides Idris' core data definitions and utility code.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

29 TypeSynonymInstances, PatternGuards #-}

310

4−module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where

11+module Idris.AbsSyntax(

12+ module Idris.AbsSyntax

13+ , module Idris.AbsSyntaxTree

14+ ) where

515

616import Idris.Core.TT

717import Idris.Core.Evaluate

src/Idris/AbsSyntaxTree.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.AbsSyntaxTree

3+Description : Core data definitions used in Idris.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

29 DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}

310

src/Idris/Apropos.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Apropos

3+Description : Search loaded Idris code and named modules for things.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.Apropos (apropos, aproposModules) where

29

310import Idris.AbsSyntax

src/Idris/CaseSplit.hs+27−21

@@ -1,11 +1,31 @@

1+{-|

2+Module : Idris.CaseSplit

3+Description : Module to provide case split functionality.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+Given a pattern clause and a variable 'n', elaborate the clause and find the

9+type of 'n'.

10+

11+Make new pattern clauses by replacing 'n' with all the possibly constructors

12+applied to '_', and replacing all other variables with '_' in order to

13+resolve other dependencies.

14+

15+Finally, merge the generated patterns with the original, by matching.

16+Always take the "more specific" argument when there is a discrepancy, i.e.

17+names over '_', patterns over names, etc.

18+

19+-}

120{-# LANGUAGE PatternGuards #-}

221

3−module Idris.CaseSplit(splitOnLine, replaceSplits,

4− getClause, getProofClause,

5− mkWith,

6− nameMissing,

7− getUniq, nameRoot) where

8−-- splitting a variable in a pattern clause

22+module Idris.CaseSplit(

23+ splitOnLine, replaceSplits

24+ , getClause, getProofClause

25+ , mkWith

26+ , nameMissing

27+ , getUniq, nameRoot

28+ ) where

929

1030import Idris.AbsSyntax

1131import Idris.AbsSyntaxTree (Idris, IState, PTerm)

@@ -36,20 +56,6 @@ import Text.Trifecta.Delta

3656

3757import Debug.Trace

3858

39−{-

40−

41−Given a pattern clause and a variable 'n', elaborate the clause and find the

42−type of 'n'.

43−

44−Make new pattern clauses by replacing 'n' with all the possibly constructors

45−applied to '_', and replacing all other variables with '_' in order to

46−resolve other dependencies.

47−

48−Finally, merge the generated patterns with the original, by matching.

49−Always take the "more specific" argument when there is a discrepancy, i.e.

50−names over '_', patterns over names, etc.

51−-}

52−

5359-- | Given a variable to split, and a term application, return a list

5460-- of variable updates, paired with a flag to say whether the given

5561-- update typechecks (False = impossible) if the flag is 'False' the

@@ -289,7 +295,7 @@ replaceSplits l ups impossible

289295 updateRHSs 1 (map (rep ist (expandBraces l)) ups)

290296 where

291297 rep ist str [] = str ++ "\n"

292− rep ist str ((n, tm) : ups)

298+ rep ist str ((n, tm) : ups)

293299 = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups

294300

295301 updateRHSs i [] = return []

src/Idris/Chaser.hs+12−1

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

1−module Idris.Chaser(buildTree, getImports, getModuleFiles, ModuleTree(..)) where

1+{-|

2+Module : Idris.Chaser

3+Description : Module chaser to determine cycles and import modules.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+module Idris.Chaser(

9+ buildTree, getImports

10+ , getModuleFiles

11+ , ModuleTree(..)

12+ ) where

213

314import Idris.Core.TT

415import Idris.Parser

src/Idris/CmdOptions.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.CmdOptions

3+Description : CLI for the Idris executable.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE Arrows #-}

29module Idris.CmdOptions where

310

src/Idris/Colours.hs+14−6

@@ -1,10 +1,18 @@

1+{-|

2+Module : Idris.Colours

3+Description : Support for colours within Idris.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.Colours (

2− IdrisColour(..),

3− ColourTheme(..),

4− defaultTheme,

5− colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,

6− colouriseType, colouriseFun, colouriseData, colouriseKeyword,

7− colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise) where

9+ IdrisColour(..)

10+ , ColourTheme(..)

11+ , defaultTheme

12+ , colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate

13+ , colouriseType, colouriseFun, colouriseData, colouriseKeyword

14+ , colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise

15+ ) where

816

917import System.Console.ANSI

1018import System.IO (Handle)

src/Idris/Completion.hs+7−1

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

1−-- | Support for command-line completion at the REPL and in the prover

1+{-|

2+Module : Idris.Completion

3+Description : Support for command-line completion at the REPL and in the prover.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

28module Idris.Completion (replCompletion, proverCompletion) where

39

410import Idris.Core.Evaluate (ctxtAlist)

src/Idris/Core/Binary.hs+10−6

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

1+{-|

2+Module : Idris.Core.Binary

3+Description : Binary instances for the core datatypes

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

2−

3−{-| Binary instances for the core datatypes -}

49module Idris.Core.Binary where

510

611import Control.Applicative ((<*>), (<$>))

@@ -271,7 +276,7 @@ instance Binary a => Binary (Err' a) where

271276

272277instance Binary FC where

273278 put x =

274− case x of

279+ case x of

275280 (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0

276281 put x1

277282 put (x2 * 65536 + x3)

@@ -589,7 +594,7 @@ instance Binary UExp where

589594 put x = case x of

590595 UVar t -> do putWord8 0

591596 put ((-1) :: Int) -- TMP HACK!

592− UVal t -> do putWord8 1

597+ UVal t -> do putWord8 1

593598 put t

594599

595600 get = do i <- getWord8

@@ -653,7 +658,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

653658 x2 <- getWord8

654659 return (Proj x1 ((fromEnum x2)-1))

655660 6 -> return Erased

656− 7 -> do x1 <- get

661+ 7 -> do x1 <- get

657662 return (TType x1)

658663 8 -> return Impossible

659664 9 -> do x1 <- get

@@ -661,4 +666,3 @@ instance {- (Binary n) => -} Binary (TT Name) where

661666 10 -> do x1 <- get

662667 return (UType x1)

663668 _ -> error "Corrupted binary data for TT"

664−

src/Idris/Core/CaseTree.hs+26−16

@@ -1,9 +1,31 @@

1+{-|

2+Module : Idris.Core.CaseTree

3+Description : Module to define and interact with case trees.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+Note: The case-tree elaborator only produces (Case n alts)-cases;

9+in other words, it never inspects anything else than variables.

10+

11+ProjCase is a special powerful case construct that allows inspection

12+of compound terms. Occurrences of ProjCase arise no earlier than

13+in the function `prune` as a means of optimisation

14+of already built case trees.

15+

16+While the intermediate representation (follows in the pipeline, named LExp)

17+allows casing on arbitrary terms, here we choose to maintain the distinction

18+in order to allow for better optimisation opportunities.

19+

20+-}

121{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

222

3−module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo,

4− Phase(..), CaseTree, CaseType(..),

5− simpleCase, small, namesUsed, findCalls, findUsedArgs,

6− substSC, substAlt, mkForce) where

23+module Idris.Core.CaseTree (

24+ CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo

25+ , Phase(..), CaseTree, CaseType(..)

26+ , simpleCase, small, namesUsed, findCalls, findUsedArgs

27+ , substSC, substAlt, mkForce

28+ ) where

729

830import Idris.Core.TT

931

@@ -18,18 +40,6 @@ import Debug.Trace

1840data CaseDef = CaseDef [Name] !SC [Term]

1941 deriving Show

2042

21−-- Note: The case-tree elaborator only produces (Case n alts)-cases;

22−-- in other words, it never inspects anything else than variables.

23−--

24−-- ProjCase is a special powerful case construct that allows inspection

25−-- of compound terms. Occurrences of ProjCase arise no earlier than

26−-- in the function `prune` as a means of optimisation

27−-- of already built case trees.

28−--

29−-- While the intermediate representation (follows in the pipeline, named LExp)

30−-- allows casing on arbitrary terms, here we choose to maintain the distinction

31−-- in order to allow for better optimisation opportunities.

32−--

3343data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first

3444 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection

3545 | STerm !t

src/Idris/Core/Constraints.hs+8−2

@@ -1,7 +1,13 @@

1−-- | Check universe constraints.

1+{-|

2+Module : Idris.Core.Constraints

3+Description : Check universe constraints.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

28module Idris.Core.Constraints ( ucheck ) where

39

4−import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),

10+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),

511 ConstraintFC(..), Err'(..) )

612

713import Control.Applicative

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

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Core.DeepSeq

3+Description : Marshalling information for TT.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE BangPatterns, ViewPatterns #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

310

@@ -241,14 +248,14 @@ instance NFData Accessibility where

241248 rnf Hidden = ()

242249 rnf Private = ()

243250

244−

251+

245252instance NFData Totality where

246253 rnf (Total x1) = rnf x1 `seq` ()

247254 rnf Productive = ()

248255 rnf (Partial x1) = rnf x1 `seq` ()

249256 rnf Unchecked = ()

250257 rnf Generated = ()

251−

258+

252259instance NFData PReason where

253260 rnf (Other x1) = rnf x1 `seq` ()

254261 rnf Itself = ()

@@ -274,7 +281,7 @@ instance NFData Def where

274281

275282instance NFData CaseInfo where

276283 rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

277−

284+

278285instance NFData CaseDefs where

279286 rnf (CaseDefs x1 x2 x3 x4)

280287 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/Core/Elaborate.hs+36−31

@@ -1,15 +1,20 @@

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

2−

3−{- A high level language of tactic composition, for building

4− elaborators from a high level language into the core theory.

5−

6− This is our interface to proof construction, rather than

7− ProofState, because this gives us a language to build derived

8− tactics out of the primitives.

1+{-|

2+Module : Idris.Core.Elaborate

3+Description : A high level language of tactic composition, for building elaborators from a high level language into the core theory.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+This is our interface to proof construction, rather than ProofState,

9+because this gives us a language to build derived tactics out of the

10+primitives.

911-}

1012

11−module Idris.Core.Elaborate(module Idris.Core.Elaborate,

12− module Idris.Core.ProofState) where

13+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

14+module Idris.Core.Elaborate (

15+ module Idris.Core.Elaborate

16+ , module Idris.Core.ProofState

17+ ) where

1318

1419import Idris.Core.ProofState

1520import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,

@@ -51,7 +56,7 @@ explicit n = do ES (p, a) s m <- get

5156 let p' = p { dontunify = n : dontunify p }

5257 put (ES (p', a) s m)

5358

54−-- Add a name that's okay to use in proof search (typically either because

59+-- Add a name that's okay to use in proof search (typically either because

5560-- it was given explicitly on the lhs, or intrduced as an explicit lambda

5661-- or let binding)

5762addPSname :: Name -> Elab' aux ()

@@ -78,11 +83,11 @@ loadState = do (ES p s e) <- get

7883getNameFrom :: Name -> Elab' aux Name

7984getNameFrom n = do (ES (p, a) s e) <- get

8085 let next = nextname p

81− let p' = p { nextname = next + 1 }

86+ let p' = p { nextname = next + 1 }

8287 put (ES (p', a) s e)

8388 let n' = case n of

8489 UN x -> MN (next+100) x

85− MN i x -> if i == 99999

90+ MN i x -> if i == 99999

8691 then MN (next+500) x

8792 else MN (next+100) x

8893 NS (UN x) s -> MN (next+100) x

@@ -97,7 +102,7 @@ setNextName = do env <- get_env

97102

98103initNextNameFrom :: [Name] -> Elab' aux ()

99104initNextNameFrom ns = do ES (p, a) s e <- get

100− let n' = maxName (nextname p) ns

105+ let n' = maxName (nextname p) ns

101106 put (ES (p { nextname = n' }, a) s e)

102107 where

103108 maxName m ((MN i _) : xs) = maxName (max m i) xs

@@ -124,7 +129,7 @@ errAt thing n ty = transformErr (Elaborating thing n ty)

124129

125130

126131erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)

127−erunAux f elab

132+erunAux f elab

128133 = do s <- get

129134 case runStateT elab s of

130135 OK (a, s') -> do put s'

@@ -489,16 +494,16 @@ dotterm = do ES (p, a) s m <- get

489494 tm <- get_term

490495 case holes p of

491496 [] -> return ()

492− (h : hs) ->

497+ (h : hs) ->

493498 do let outer = findOuter h [] tm

494499 let p' = p { dotted = (h, outer) : dotted p }

495−-- trace ("DOTTING " ++ show (h, outer) ++ "\n" ++

500+-- trace ("DOTTING " ++ show (h, outer) ++ "\n" ++

496501-- show tm) $

497502 put $ ES (p', a) s m

498503 where

499504 findOuter h env (P _ n _) | h == n = env

500505 findOuter h env (Bind n b sc)

501− = union (foB b)

506+ = union (foB b)

502507 (findOuter h env (instantiate (P Bound n (binderTy b)) sc))

503508 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)

504509 foB (Let t v) = union (findOuter h env t) (findOuter h env v)

@@ -506,7 +511,7 @@ dotterm = do ES (p, a) s m <- get

506511 findOuter h env (App _ f a)

507512 = union (findOuter h env f) (findOuter h env a)

508513 findOuter h env _ = []

509−

514+

510515

511516get_dotterm :: Elab' aux [(Name, [Name])]

512517get_dotterm = do ES (p, a) s m <- get

@@ -566,8 +571,8 @@ prepare_apply fn imps =

566571 env <- get_env

567572 -- let claims = getArgs ty imps

568573 -- claims <- mkClaims (normalise ctxt env ty) imps []

569− claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $

570− mkClaims (finalise ty)

574+ claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $

575+ mkClaims (finalise ty)

571576 (normalise ctxt env (finalise ty))

572577 imps [] (map fst env)

573578 ES (p, a) s prev <- get

@@ -583,7 +588,7 @@ prepare_apply fn imps =

583588 -> [(Name, Name)] -- ^ Accumulator for produced claims

584589 -> [Name] -- ^ Hypotheses

585590 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

586− mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) (i : is) claims hs =

591+ mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) (i : is) claims hs =

587592 do let t = rebind hs t_in

588593 n <- getNameFrom (mkMN n')

589594-- when (null claims) (start_unify n)

@@ -657,7 +662,7 @@ apply' fillt fn imps =

657662

658663 getNonUnify acc [] _ = acc

659664 getNonUnify acc _ [] = acc

660− getNonUnify acc ((i,_):is) ((a, t):as)

665+ getNonUnify acc ((i,_):is) ((a, t):as)

661666 | i = getNonUnify acc is as

662667 | otherwise = getNonUnify (t : acc) is as

663668

@@ -787,7 +792,7 @@ infer_app infer fun arg str =

787792 end_unify

788793

789794dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

790−dep_app fun arg str =

795+dep_app fun arg str =

791796 do a <- getNameFrom (sMN 0 "__argTy")

792797 b <- getNameFrom (sMN 0 "__retTy")

793798 fty <- getNameFrom (sMN 0 "__fnTy")

@@ -800,13 +805,13 @@ dep_app fun arg str =

800805 g <- goal

801806 start_unify s

802807 claim s (Var a)

803−

808+

804809 prep_fill f [s]

805810 focus f; attack; fun

806811 end_unify

807812 fty <- goal

808813 solve

809− focus s; attack;

814+ focus s; attack;

810815 ctxt <- get_context

811816 env <- get_env

812817 case normalise ctxt env fty of

@@ -856,7 +861,7 @@ no_errors tac err

856861 ((x, y, _, env, inerr, while, _) : _) ->

857862 let (xp, yp) = getProvenance inerr

858863 env' = map (\(x, b) -> (x, binderTy b)) env in

859− lift $ tfail $

864+ lift $ tfail $

860865 case err of

861866 Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0

862867 Just e -> e

@@ -867,7 +872,7 @@ try :: Elab' aux a -> Elab' aux a -> Elab' aux a

867872try t1 t2 = try' t1 t2 False

868873

869874handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a

870−handleError p t1 t2

875+handleError p t1 t2

871876 = do s <- get

872877 ps <- get_probs

873878 case runStateT t1 s of

@@ -907,7 +912,7 @@ try' t1 t2 proofSearch

907912 recoverableErr _ = True

908913

909914tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

910−tryCatch t1 t2

915+tryCatch t1 t2

911916 = do s <- get

912917 ps <- get_probs

913918 ulog <- getUnifyLog

@@ -953,7 +958,7 @@ tryAll' constrok xs = doAll [] 999999 xs

953958 ivs <- get_instances

954959 case prunStateT pmax True ps (if constrok then Nothing

955960 else Just ivs) x s of

956− OK ((v, newps, probs), s') ->

961+ OK ((v, newps, probs), s') ->

957962 do let cs' = if (newps < pmax)

958963 then [do put s'; return $! v]

959964 else (do put s'; return $! v) : cs

@@ -980,7 +985,7 @@ prunStateT pmax zok ps ivs x s

980985 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

981986 then case reverse (problems p) of

982987 ((_,_,_,_,e,_,_):_) -> Error e

983− else if ibad

988+ else if ibad

984989 then Error (InternalMsg "Constraint introduced in disambiguation")

985990 else OK ((v, newpmax, problems p), s')

986991 Error e -> Error e

src/Idris/Core/Evaluate.hs+17−10

@@ -1,8 +1,15 @@

1+{-|

2+Module : Idris.Core.Evaluate

3+Description : Evaluate Idris expressions.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,

29 PatternGuards #-}

310{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

411

5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

12+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

613 normaliseAll, normaliseBlocking, toValue, quoteTerm,

714 rt_simplify, simplify, specialise, hnf, convEq, convEq',

815 Def(..), CaseInfo(..), CaseDefs(..),

@@ -12,7 +19,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

1219 addDatatype, addCasedef, simplifyCasedef, addOperator,

1320 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

1421 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

15− mapDefCtxt,

22+ mapDefCtxt,

1623 lookupTotal, lookupTotalExact, lookupInjectiveExact,

1724 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

1825 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

@@ -103,7 +110,7 @@ normaliseTrace tr ctxt env t

103110 quote 0 val) initEval

104111

105112toValue :: Context -> Env -> TT Name -> Value

106−toValue ctxt env t

113+toValue ctxt env t

107114 = evalState (eval False ctxt [] (map finalEntry env) t []) initEval

108115

109116quoteTerm :: Value -> TT Name

@@ -596,9 +603,9 @@ convEq ctxt holes topx topy = ceq [] topx topy where

596603 | x `elem` holes || y `elem` holes = return True

597604 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

598605 | otherwise = sameDefs ps x y

599− ceq ps x (Bind n (Lam t) (App _ y (V 0)))

606+ ceq ps x (Bind n (Lam t) (App _ y (V 0)))

600607 = ceq ps x (substV (P Bound n t) y)

601− ceq ps (Bind n (Lam t) (App _ x (V 0))) y

608+ ceq ps (Bind n (Lam t) (App _ x (V 0))) y

602609 = ceq ps (substV (P Bound n t) x) y

603610 ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))

604611 | n == n' = ceq ps x y

@@ -746,9 +753,9 @@ instance Show Def where

746753-- Hidden => Programs can't access the name at all

747754-- Public => Programs can access the name and use at will

748755-- Frozen => Programs can access the name, which doesn't reduce

749−-- Private => Programs can't access the name, doesn't reduce internally

756+-- Private => Programs can't access the name, doesn't reduce internally

750757

751−data Accessibility = Hidden | Public | Frozen | Private

758+data Accessibility = Hidden | Public | Frozen | Private

752759 deriving (Eq, Ord)

753760{-!

754761deriving instance NFData Accessibility

@@ -993,7 +1000,7 @@ lookupTyName n ctxt = do

9931000

9941001-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.

9951002lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)

996−lookupTyNameExact n ctxt = listToMaybe [ (nm, v) | (nm, v) <- lookupTyName n ctxt, nm == n ]

1003+lookupTyNameExact n ctxt = listToMaybe [ (nm, v) | (nm, v) <- lookupTyName n ctxt, nm == n ]

9971004

9981005-- | Get the types that match some name

9991006lookupTy :: Name -> Context -> [Type]

@@ -1048,7 +1055,7 @@ lookupP = lookupP_all False False

10481055

10491056lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]

10501057lookupP_all all exact n ctxt

1051− = do (n', def) <- names

1058+ = do (n', def) <- names

10521059 p <- case def of

10531060 (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)

10541061 (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)

@@ -1060,7 +1067,7 @@ lookupP_all all exact n ctxt

10601067 _ -> return (fst p)

10611068 where

10621069 names = let ns = lookupCtxtName n (definitions ctxt) in

1063− if exact

1070+ if exact

10641071 then filter (\ (n', d) -> n' == n) ns

10651072 else ns

10661073

src/Idris/Core/Execute.hs+22−14

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.Core.Execute

3+Description : Execute Idris code and deal with FFI.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}

210{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

311module Idris.Core.Execute (execute) where

@@ -112,7 +120,7 @@ toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

112120 return $ normalise ctxt env' tm

113121 where toBinder (n, v) = do v' <- toTT v

114122 return (n, Let Erased v')

115−toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."

123+toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."

116124toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."

117125

118126unApplyV :: ExecVal -> (ExecVal, [ExecVal])

@@ -251,7 +259,7 @@ execApp env ctxt c@(EP (TCon _ arity) n _) args =

251259 let restArgs = drop arity args

252260 execApp env ctxt (mkEApp c args') restArgs

253261

254−execApp env ctxt f@(EP _ n _) args

262+execApp env ctxt f@(EP _ n _) args

255263 | Just (res, rest) <- getOp n args = do r <- res

256264 execApp env ctxt r rest

257265execApp env ctxt f@(EP _ n _) args =

@@ -388,7 +396,7 @@ execForeign env ctxt arity ty fn xs onfail

388396

389397-- Right now, there's no way to send command-line arguments to the executor,

390398-- so just return 0.

391−execForeign env ctxt arity ty fn xs onfail

399+execForeign env ctxt arity ty fn xs onfail

392400 | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs

393401 = let res = ioWrap . EConstant . I $ 0

394402 in execApp env ctxt res (drop arity xs)

@@ -410,8 +418,8 @@ splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits

410418 = Just (toFDesc l, r)

411419splitArg _ = Nothing

412420

413−toFDesc tm

414− | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)

421+toFDesc tm

422+ | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)

415423 | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)

416424toFDesc _ = FUnknown

417425

@@ -432,7 +440,7 @@ upio = sUN "unsafePerformPrimIO"

432440delay = sUN "Delay"

433441force = sUN "Force"

434442

435−-- | Look up primitive operations in the global table and transform

443+-- | Look up primitive operations in the global table and transform

436444-- them into ExecVal functions

437445getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])

438446getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)

@@ -463,14 +471,14 @@ getOp fn (_ : EHandle h : xs)

463471getOp fn (_ : arg : xs)

464472 | fn == prf =

465473 Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)

466−getOp n args = do (arity, prim) <- getPrim n primitives

467− if (length args >= arity)

474+getOp n args = do (arity, prim) <- getPrim n primitives

475+ if (length args >= arity)

468476 then do res <- applyPrim prim (take arity args)

469477 Just (res, drop arity args)

470478 else Nothing

471479 where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)

472480 getPrim n [] = Nothing

473− getPrim n ((Prim pn _ arity def _ _) : prims)

481+ getPrim n ((Prim pn _ arity def _ _) : prims)

474482 | n == pn = Just (arity, execPrim def)

475483 | otherwise = getPrim n prims

476484

@@ -534,15 +542,15 @@ chooseAlt _ [] = Nothing

534542data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show

535543

536544toFType :: FDesc -> FType

537−toFType (FCon c)

545+toFType (FCon c)

538546 | c == sUN "C_Str" = FString

539547 | c == sUN "C_Float" = FArith ATFloat

540548 | c == sUN "C_Ptr" = FPtr

541549 | c == sUN "C_MPtr" = FManagedPtr

542550 | c == sUN "C_Unit" = FUnit

543−toFType (FApp c [_,ity])

551+toFType (FApp c [_,ity])

544552 | c == sUN "C_IntT" = FArith (toAType ity)

545− where toAType (FCon i)

553+ where toAType (FCon i)

546554 | i == sUN "C_IntChar" = ATInt ITChar

547555 | i == sUN "C_IntNative" = ATInt ITNative

548556 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)

@@ -551,14 +559,14 @@ toFType (FApp c [_,ity])

551559 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)

552560 toAType t = error (show t ++ " not defined in toAType")

553561

554−toFType (FApp c [_])

562+toFType (FApp c [_])

555563 | c == sUN "C_Any" = FAny

556564toFType t = error (show t ++ " not defined in toFType")

557565

558566call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

559567call (FFun name argTypes retType) args =

560568 do fn <- findForeign name

561− maybe (return Nothing)

569+ maybe (return Nothing)

562570 (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn

563571 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal

564572 call' (Fun _ h) args (FArith (ATInt ITNative)) = do

src/Idris/Core/ProofState.hs+37−28

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

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

2−

3−{- Implements a proof state, some primitive tactics for manipulating

4− proofs, and some high level commands for introducing new theorems,

5− evaluation/checking inside the proof system, etc. --}

1+{-|

2+Module : Idris.Core.ProofState

3+Description : Proof state implementation.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+Implements a proof state, some primitive tactics for manipulating

9+proofs, and some high level commands for introducing new theorems,

10+evaluation/checking inside the proof system, etc.

11+-}

612

7−module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8− Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,

9− doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where

13+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

14+module Idris.Core.ProofState(

15+ ProofState(..), newProof, envAtFocus, goalAtFocus

16+ , Tactic(..), Goal(..), processTactic, nowElaboratingPS

17+ , doneElaboratingAppPS, doneElaboratingArgPS, dropGiven

18+ , keepGiven, getProvenance

19+ ) where

1020

1121import Idris.Core.Typecheck

1222import Idris.Core.Evaluate

@@ -134,7 +144,7 @@ instance Pretty ProofState OutputAnnotation where

134144 pretty (thname ps) <+> colon <+> text " no more goals."

135145 pretty ps | (h : hs) <- holes ps =

136146 let tm = pterm ps

137− OK g = goal (Just h) tm

147+ OK g = goal (Just h) tm

138148 nm = thname ps in

139149 let wkEnv = premises g in

140150 text "Other goals" <+> colon <+> pretty hs <+>

@@ -160,8 +170,8 @@ holeName i = sMN i "hole"

160170qshow :: Fails -> String

161171qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fst env, x, y, hs)) fs)

162172

163−match_unify' :: Context -> Env ->

164− (TT Name, Maybe Provenance) ->

173+match_unify' :: Context -> Env ->

174+ (TT Name, Maybe Provenance) ->

165175 (TT Name, Maybe Provenance) ->

166176 StateT TState TC [(Name, TT Name)]

167177match_unify' ctxt env (topx, xfrom) (topy, yfrom) =

@@ -184,7 +194,7 @@ match_unify' ctxt env (topx, xfrom) (topy, yfrom) =

184194 return u

185195 Error e -> traceWhen (unifylog ps)

186196 ("No match " ++ show e) $

187− do put (ps { problems = (topx, topy, True,

197+ do put (ps { problems = (topx, topy, True,

188198 env, e, while, Match) :

189199 problems ps })

190200 return []

@@ -217,8 +227,8 @@ dropSwaps (p@(x, P _ y _) : xs) | solvedIn y x xs = dropSwaps xs

217227 solvedIn y x (_ : xs) = solvedIn y x xs

218228dropSwaps (p : xs) = p : dropSwaps xs

219229

220−unify' :: Context -> Env ->

221− (TT Name, Maybe Provenance) ->

230+unify' :: Context -> Env ->

231+ (TT Name, Maybe Provenance) ->

222232 (TT Name, Maybe Provenance) ->

223233 StateT TState TC [(Name, TT Name)]

224234unify' ctxt env (topx, xfrom) (topy, yfrom) =

@@ -539,7 +549,7 @@ match_fill guess ctxt env (Bind x (Hole ty) sc) =

539549 do (val, valty) <- lift $ check ctxt env guess

540550-- let valtyn = normalise ctxt env valty

541551-- let tyn = normalise ctxt env ty

542− ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)

552+ ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)

543553 (ty, Just ExpectedType)

544554 ps <- get

545555 let (uh, uns) = unified ps

@@ -558,7 +568,7 @@ complete_fill :: RunTactic

558568complete_fill ctxt env (Bind x (Guess ty val) sc) =

559569 do let guess = forget val

560570 (val', valty) <- lift $ check ctxt env guess

561− ns <- unify' ctxt env (valty, Just $ SourceTerm val')

571+ ns <- unify' ctxt env (valty, Just $ SourceTerm val')

562572 (ty, Just ExpectedType)

563573 ps <- get

564574 let (uh, uns) = unified ps

@@ -577,7 +587,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

577587 dropdots <-

578588 case lookup x (notunified ps) of

579589 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

580− do match_unify' ctxt env (tm, Just InferredVal)

590+ do match_unify' ctxt env (tm, Just InferredVal)

581591 (val, Just GivenVal)

582592 return [x]

583593 _ -> return []

@@ -608,12 +618,12 @@ solve ctxt env (Bind x (Guess ty val) sc)

608618 tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)

609619 tryLock hs t@(Bind n (Hole _) sc) = (t, False)

610620 tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)

611− tryLock hs t@(Bind n (Let ty val) sc)

621+ tryLock hs t@(Bind n (Let ty val) sc)

612622 = let (ty', tyl) = tryLock hs ty

613623 (val', vall) = tryLock hs val

614624 (sc', scl) = tryLock hs sc in

615625 (Bind n (Let ty' val') sc', tyl && vall && scl)

616− tryLock hs t@(Bind n b sc)

626+ tryLock hs t@(Bind n b sc)

617627 = let (bt', btl) = tryLock hs (binderTy b)

618628 (val', vall) = tryLock hs val

619629 (sc', scl) = tryLock hs sc in

@@ -895,7 +905,7 @@ keepGiven du (u : us) hs = keepGiven du us hs

895905

896906updateEnv [] e = e

897907updateEnv ns [] = []

898−updateEnv ns ((n, b) : env)

908+updateEnv ns ((n, b) : env)

899909 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

900910

901911updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t

@@ -907,7 +917,7 @@ updateError ns (Elaborating s n ty e) = Elaborating s n ty (updateError ns e)

907917updateError ns (ElaboratingArg f a env e)

908918 = ElaboratingArg f a env (updateError ns e)

909919updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

910− = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)

920+ = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)

911921 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

912922updateError ns e = e

913923

@@ -940,7 +950,7 @@ getProvenance _ = (Nothing, Nothing)

940950

941951setReady (x, y, _, env, err, c, at) = (x, y, True, env, err, c, at)

942952

943−updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

953+updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

944954 -> ([(Name, TT Name)], Fails)

945955-- updateProblems ctxt [] ps inj holes = ([], ps)

946956updateProblems ps updates probs = rec 10 updates probs

@@ -966,8 +976,8 @@ updateProblems ps updates probs = rec 10 updates probs

966976 (lp, rp) = getProvenance err

967977 err' = updateError ns err

968978 env' = updateEnv ns env in

969− if newx || newy || ready ||

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

979+ if newx || newy || ready ||

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

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

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

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

@@ -980,11 +990,11 @@ updateProblems ps updates probs = rec 10 updates probs

980990 updateNs ns (x, y, t, env, err, fc, fa)

981991 = let (x', newx) = updateSolvedTerm' ns x

982992 (y', newy) = updateSolvedTerm' ns y in

983− (x', y', newx || newy,

993+ (x', y', newx || newy,

984994 updateEnv ns env, updateError ns err, fc, fa)

985995

986996-- attempt to solve remaining problems with match_unify

987−matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

997+matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

988998 -> ([(Name, TT Name)], Fails)

989999matchProblems all ps updates probs = up updates probs where

9901000 hs = holes ps

@@ -1085,7 +1095,7 @@ processTactic t ps

10851095 -- apply them here

10861096 let ns' = dropGiven (dontunify ps') ns_in (holes ps')

10871097 let pterm'' = updateSolved ns' (pterm ps')

1088− traceWhen (unifylog ps)

1098+ traceWhen (unifylog ps)

10891099 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++

10901100 "(Toplevel) Dropping holes: " ++ show (map fst ns') ++ "\n" ++

10911101 "Holes were: " ++ show (holes ps')) $

@@ -1139,4 +1149,3 @@ process t h = tactic (Just h) (mktac t)

11391149 mktac (MoveLast n) = movelast n

11401150 mktac (UnifyGoal r) = unifyGoal r

11411151 mktac (UnifyTerms x y) = unifyTerms x y

1142−

src/Idris/Core/ProofTerm.hs+31−28

@@ -1,16 +1,20 @@

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

2−

3−{- | Implements a proof state, some primitive tactics for manipulating

4−proofs, and some high level commands for introducing new theorems,

5−evaluation/checking inside the proof system, etc.

1+{-|

2+Module : Idris.Core.ProofTerm

3+Description : Proof term. implementation and utilities.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

67-}

78

8−module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

9− resetProofTerm,

10− updateSolved, updateSolvedTerm, updateSolvedTerm',

11− bound_in, bound_in_term, refocus, updsubst,

12− Hole, RunTactic',

13− goal, atHole) where

9+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

10+module Idris.Core.ProofTerm(

11+ ProofTerm, Goal(..), mkProofTerm, getProofTerm

12+ , resetProofTerm

13+ , updateSolved, updateSolvedTerm, updateSolvedTerm'

14+ , bound_in, bound_in_term, refocus, updsubst

15+ , Hole, RunTactic'

16+ , goal, atHole

17+ ) where

1418

1519import Idris.Core.Typecheck

1620import Idris.Core.Evaluate

@@ -72,7 +76,7 @@ rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)

7276-- are crossed, and the actual binding term.

7377findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

7478findHole n env t = fh' env Top t where

75− fh' env path tm@(Bind x h sc)

79+ fh' env path tm@(Bind x h sc)

7680 | hole h && n == x = Just (path, env, tm)

7781 fh' env path (App Complete _ _) = Nothing

7882 fh' env path (App s f a)

@@ -114,7 +118,7 @@ refocus' (Just n) pt@(PT path env tm ups)

114118 -- First look for the hole in the proof term as-is

115119 | Just (p', env', tm') <- findHole n env tm

116120 = PT (replaceTop p' path) env' tm' ups

117− -- If it's not there, rebuild and look from the top

121+ -- If it's not there, rebuild and look from the top

118122 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))

119123 = PT p' env' tm' []

120124 | otherwise = pt

@@ -128,7 +132,7 @@ mkProofTerm :: Term -> ProofTerm

128132mkProofTerm tm = PT Top [] tm []

129133

130134getProofTerm :: ProofTerm -> Term

131−getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

135+getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

132136

133137resetProofTerm :: ProofTerm -> ProofTerm

134138resetProofTerm = mkProofTerm . getProofTerm

@@ -183,11 +187,11 @@ updateSolvedTerm' xs x = updateSolved' xs x where

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

184188 updateSolved' xs t = (t, False)

185189

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

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

187191 (v', uv) = updateSolved' xs v in

188192 if ut || uv then (Let t' v', True)

189193 else (b, False)

190− updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t

194+ updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t

191195 (v', uv) = updateSolved' xs v in

192196 if ut || uv then (Guess t' v', True)

193197 else (b, False)

@@ -261,7 +265,7 @@ updateSolvedPath ns t@(AppL Complete _ _) = t

261265updateSolvedPath ns t@(AppR Complete _ _) = t

262266updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)

263267updateSolvedPath ns (AppR s l p) = AppR s (updateSolvedTerm ns l) (updateSolvedPath ns p)

264−updateSolvedPath ns (InBind n b sc)

268+updateSolvedPath ns (InBind n b sc)

265269 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)

266270 where

267271 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)

@@ -277,18 +281,18 @@ updateSolvedPath ns (InScope n (Hole ty) t)

277281updateSolvedPath ns (InScope n b sc)

278282 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)

279283

280−updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

281−updateSolved xs pt@(PT path env sub ups)

282− = PT path -- (updateSolvedPath xs path)

283− (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))

284− (updateSolvedTerm xs sub)

284+updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

285+updateSolved xs pt@(PT path env sub ups)

286+ = PT path -- (updateSolvedPath xs path)

287+ (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))

288+ (updateSolvedTerm xs sub)

285289 (ups ++ xs)

286290

287291goal :: Hole -> ProofTerm -> TC Goal

288−goal h pt@(PT path env sub ups)

292+goal h pt@(PT path env sub ups)

289293-- | OK ginf <- g env sub = return ginf

290294 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))

291− where

295+ where

292296 g :: Env -> Term -> TC Goal

293297 g env (Bind n b@(Guess _ _) sc)

294298 | same h n = return $ GD env b

@@ -297,7 +301,7 @@ goal h pt@(PT path env sub ups)

297301 g env (Bind n b sc) | hole b && same h n = return $ GD env b

298302 | otherwise

299303 = g ((n, b):env) sc `mplus` gb env b

300− g env (App Complete f a) = fail "Can't find hole"

304+ g env (App Complete f a) = fail "Can't find hole"

301305 g env (App _ f a) = g env a `mplus` g env f

302306 g env t = fail "Can't find hole"

303307

@@ -305,9 +309,9 @@ goal h pt@(PT path env sub ups)

305309 gb env (Guess t v) = g env v `mplus` g env t

306310 gb env t = g env (binderTy t)

307311

308−atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

312+atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

309313 StateT a TC (ProofTerm, Bool)

310−atHole h f c e pt -- @(PT path env sub)

314+atHole h f c e pt -- @(PT path env sub)

311315 = do let PT path env sub ups = refocus h pt

312316 (tm, u) <- atH f c env sub

313317 return (PT path env tm ups, u)

@@ -362,4 +366,3 @@ bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

362366 bi b = bound_in_term (binderTy b)

363367bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a

364368bound_in_term _ = []

365−

src/Idris/Core/TT.hs+39−31

@@ -1,7 +1,11 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,

2− DeriveDataTypeable, PatternGuards #-}

3−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

4−{-| TT is the core language of Idris. The language has:

1+{-|

2+Module : Idris.Core.TT

3+Description : The core language of Idris, TT.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+TT is the core language of Idris. The language has:

59

610 * Full dependent types

711

@@ -18,30 +22,34 @@

1822 * We have a simple collection of tactics which we use to elaborate source

1923 programs with implicit syntax into fully explicit terms.

2024-}

21−

22−module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..),

23− ConstraintFC(..), DataOpt(..), DataOpts(..), Datatype(..),

24− Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..),

25− FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..),

26− NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..),

27− Provenance(..), Raw(..), SpecialName(..), TC(..), Term(..),

28− TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..),

29− UConstraint(..), UCs(..), UExp(..), Universe(..),

30− addAlist, addBinder, addDef, allTTNames, arity, bindAll,

31− bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact,

32− discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname,

33− fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv,

34− freeNames, getArgTys, getRetTy, implicitable, instantiate,

35− intTyName, isInjective, isTypeConst, liftPats, lookupCtxt,

36− lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth,

37− nextName, noOccurrence, nsroot, occurrences, orderPats,

38− pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV,

39− pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget,

40− safeForgetEnv, showCG, showEnv, showEnvDbg, showSep,

41− sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm,

42− substV, sUN, tcname, termSmallerThan, tfail, thead, tnull,

43− toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,

44− uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm) where

25+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,

26+ DeriveDataTypeable, PatternGuards #-}

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

28+module Idris.Core.TT(

29+ AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)

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

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

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

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

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

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

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

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

38+ , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact

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

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

41+ , freeNames, getArgTys, getRetTy, implicitable, instantiate

42+ , intTyName, isInjective, isTypeConst, liftPats, lookupCtxt

43+ , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth

44+ , nextName, noOccurrence, nsroot, occurrences, orderPats

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

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

47+ , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep

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

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

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

51+ , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

52+ ) where

4553

4654-- Work around AMP without CPP

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

@@ -317,7 +325,7 @@ bindTC x k = case x of

317325

318326instance Monad TC where

319327 return x = OK x

320− x >>= k = bindTC x k

328+ x >>= k = bindTC x k

321329 fail e = Error (InternalMsg e)

322330

323331instance MonadPlus TC where

@@ -386,7 +394,7 @@ instance Show Err where

386394 show (At f e) = show f ++ ":" ++ show e

387395 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

388396 show x ++ ": " ++ show e

389− show (Elaborating what n ty e) = "Elaborating " ++ what ++ show n ++

397+ show (Elaborating what n ty e) = "Elaborating " ++ what ++ show n ++

390398 showType ty ++ ":" ++ show e

391399 where

392400 showType Nothing = ""

@@ -964,7 +972,7 @@ data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,

964972 deriving (Show, Data, Typeable)

965973

966974instance Eq ConstraintFC where

967− x == y = uconstraint x == uconstraint y

975+ x == y = uconstraint x == uconstraint y

968976

969977instance Ord ConstraintFC where

970978 compare x y = compare (uconstraint x) (uconstraint y)

src/Idris/Core/Typecheck.hs+12−4

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.Core.Typecheck

3+Description : Idris' type checker.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

210 PatternGuards #-}

311

@@ -86,10 +94,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

8694 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

8795 -- If we're elaborating, we don't want the private names; if we're

8896 -- checking an already elaborated term, we do

89− | [P nt n' ty] <- lookupP_all (not holes) False n ctxt

97+ | [P nt n' ty] <- lookupP_all (not holes) False n ctxt

9098 = return (P nt n' ty, ty)

9199 -- If the names are ambiguous, require it to be fully qualified

92− | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

100+ | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

93101 = return (P nt n' ty, ty)

94102 | otherwise = do lift $ tfail $ NoSuchVariable n

95103 chk u env ap@(RApp f RType) | not holes

@@ -109,7 +117,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

109117 (Bind x (Let (TType v') (TType (UVar v))) t)

110118 return (App Complete fv (TType (UVar v)), apty)

111119 Bind x (Pi i s k) t ->

112− do (av, aty) <- chk u env RType

120+ do (av, aty) <- chk u env RType

113121 convertsC ctxt env aty s

114122 let apty = simplify initContext env

115123 (Bind x (Let aty av) t)

@@ -170,7 +178,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

170178 case (normalise ctxt env st, normalise ctxt env tt) of

171179 (TType su, TType tu) -> do

172180 when (not holes) $ do (v, cs) <- get

173− put (v, ULE su maxu :

181+ put (v, ULE su maxu :

174182 ULE tu maxu : cs)

175183 let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u

176184 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

src/Idris/Core/Unify.hs+44−34

@@ -1,7 +1,23 @@

1+{-|

2+Module : Idris.Core.Unify

3+Description : Idris' unification code.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+

8+Unification is applied inside the theorem prover. We're looking for holes

9+which can be filled in, by matching one term's normal form against another.

10+Returns a list of hole names paired with the term which solves them, and

11+a list of things which need to be injective.

12+

13+-}

114{-# LANGUAGE PatternGuards #-}

215

3−module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..),

4− unrecoverable) where

16+module Idris.Core.Unify(

17+ match_unify, unify

18+ , Fails, FailContext(..), FailAt(..)

19+ , unrecoverable

20+ ) where

521

622import Idris.Core.TT

723import Idris.Core.Evaluate

@@ -12,14 +28,8 @@ import Data.Maybe

1228import Data.List

1329import Debug.Trace

1430

15−-- Unification is applied inside the theorem prover. We're looking for holes

16−-- which can be filled in, by matching one term's normal form against another.

17−-- Returns a list of hole names paired with the term which solves them, and

18−-- a list of things which need to be injective.

19−

2031-- terms which need to be injective, with the things we're trying to unify

2132-- at the time

22−

2333data FailAt = Match | Unify

2434 deriving (Show, Eq)

2535

@@ -62,14 +72,14 @@ cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

6272-- Solve metavariables by matching terms against each other

6373-- Not really unification, of course!

6474

65−match_unify :: Context -> Env ->

66− (TT Name, Maybe Provenance) ->

75+match_unify :: Context -> Env ->

76+ (TT Name, Maybe Provenance) ->

6777 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->

6878 TC [(Name, TT Name)]

6979match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

7080 case runStateT (un [] (renameBindersTm env topx)

7181 (renameBindersTm env topy)) (UI 0 []) of

72− OK (v, UI _ []) ->

82+ OK (v, UI _ []) ->

7383 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

7484 return (map (renameBinders env) v')

7585 res ->

@@ -136,10 +146,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

136146 let r = recoverable (normalise ctxt env (binderTy x))

137147 (normalise ctxt env (binderTy y))

138148 let err = cantUnify from r (topx, xfrom) (topy, yfrom)

139− (CantUnify r (binderTy x, Nothing)

149+ (CantUnify r (binderTy x, Nothing)

140150 (binderTy y, Nothing) (Msg "") (errEnv env) s)

141151 (errEnv env) s

142− put (UI s ((binderTy x, binderTy y,

152+ put (UI s ((binderTy x, binderTy y,

143153 False,

144154 env, err, from, Match) : f))

145155 return []

@@ -236,13 +246,13 @@ trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPa

236246 followSols vs ((n, P _ t _) : ns)

237247 | Just t' <- lookup t ns

238248 = do vs' <- case t' of

239− P _ tn _ ->

249+ P _ tn _ ->

240250 if (n, tn) `elem` vs then -- cycle

241− tfail (cantUnify from False (topx, xfrom) (topy, yfrom)

251+ tfail (cantUnify from False (topx, xfrom) (topy, yfrom)

242252 (Msg "") (errEnv env) 0)

243253 else return ((n, tn) : vs)

244254 _ -> return vs

245− followSols vs' ((n, t') : ns)

255+ followSols vs' ((n, t') : ns)

246256 followSols vs (n : ns) = do ns' <- followSols vs ns

247257 return $ n : ns'

248258

@@ -260,8 +270,8 @@ hasv (App _ f a) = hasv f || hasv a

260270hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

261271hasv _ = False

262272

263−unify :: Context -> Env ->

264− (TT Name, Maybe Provenance) ->

273+unify :: Context -> Env ->

274+ (TT Name, Maybe Provenance) ->

265275 (TT Name, Maybe Provenance) ->

266276 [Name] -> [Name] -> [Name] -> [FailContext] ->

267277 TC ([(Name, TT Name)], Fails)

@@ -281,7 +291,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

281291 (UI 0 []) of

282292 OK (v, UI _ fails) ->

283293 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

284−-- trace ("OK " ++ show (topxn, topyn, v, holes)) $

294+-- trace ("OK " ++ show (topxn, topyn, v, holes)) $

285295 return (map (renameBinders env) v', reverse fails)

286296-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

287297 Error e -> tfail e

@@ -292,7 +302,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

292302

293303 injective (P (DCon _ _ _) _ _) = True

294304 injective (P (TCon _ _) _ _) = True

295− injective (P Ref n _)

305+ injective (P Ref n _)

296306 | Just i <- lookupInjectiveExact n ctxt = i

297307 injective (App _ f a) = injective f -- && injective a

298308 injective _ = False

@@ -410,8 +420,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

410420 all rigid args,

411421 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm

412422 -- && TODO: tm does not refer to any variables other than those

413− -- in 'args'

414− = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

423+ -- in 'args'

424+ = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

415425 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))

416426 where rigid (V i) = True

417427 rigid (P _ t _) = t `elem` map fst env &&

@@ -425,14 +435,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

425435 getname _ = Nothing

426436

427437 containsOnly args vs (V i) = i `elem` vs

428− containsOnly args vs (P Bound n ty)

438+ containsOnly args vs (P Bound n ty)

429439 = n `elem` args && containsOnly args vs ty

430− containsOnly args vs (P _ n ty)

440+ containsOnly args vs (P _ n ty)

431441 = not (holeIn env n || n `elem` holes)

432442 && containsOnly args vs ty

433− containsOnly args vs (App _ f a)

443+ containsOnly args vs (App _ f a)

434444 = containsOnly args vs f && containsOnly args vs a

435− containsOnly args vs (Bind _ b sc)

445+ containsOnly args vs (Bind _ b sc)

436446 = containsOnly args vs (binderTy b) &&

437447 containsOnly args (0 : map (+1) vs) sc

438448 containsOnly args vs _ = True

@@ -440,14 +450,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

440450 bindLams [] tm = tm

441451 bindLams (a : as) tm = bindLam a (bindLams as tm)

442452

443− bindLam (V i) tm = Bind (fst (env !! i))

444− (Lam (binderTy (snd (env !! i))))

453+ bindLam (V i) tm = Bind (fst (env !! i))

454+ (Lam (binderTy (snd (env !! i))))

445455 tm

446456 bindLam (P _ n ty) tm = Bind n (Lam ty) tm

447457 bindLam _ tm = error "Can't happen [non rigid bindLam]"

448458

449459 substEnv [] tm = tm

450− substEnv ((n, t) : env) tm

460+ substEnv ((n, t) : env) tm

451461 = substEnv env (substV (P Bound n (binderTy t)) tm)

452462

453463 -- remove any unnecessary lambdas (helps with type class

@@ -532,7 +542,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

532542 let ax' = hnormalise hf ctxt env (substNames hf ax)

533543 let ay' = hnormalise hf ctxt env (substNames hf ay)

534544 -- Don't normalise if we don't have to

535− ha <- uplus (un' env False bnames (substNames hf ax)

545+ ha <- uplus (un' env False bnames (substNames hf ax)

536546 (substNames hf ay))

537547 (un' env False bnames ax' ay')

538548 sc 1

@@ -607,7 +617,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

607617 = do UI s f <- get

608618 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

609619 let err = cantUnify from r

610− (topx, xfrom) (topy, yfrom)

620+ (topx, xfrom) (topy, yfrom)

611621 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

612622 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

613623 return []

@@ -616,7 +626,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

616626 unifyFail x y = do UI s f <- get

617627 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

618628 let err = cantUnify from r

619− (topx, xfrom) (topy, yfrom)

629+ (topx, xfrom) (topy, yfrom)

620630 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

621631 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

622632 lift $ tfail err

@@ -636,14 +646,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

636646 uB env bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' env False bnames tx ty

637647 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty

638648 uB env bnames (PVar tx) (PVar ty) = un' env False bnames tx ty

639− uB env bnames x y

649+ uB env bnames x y

640650 = do UI s f <- get

641651 let r = recoverable (normalise ctxt env (binderTy x))

642652 (normalise ctxt env (binderTy y))

643653 let err = cantUnify from r (topx, xfrom) (topy, yfrom)

644654 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)

645655 (errEnv env) s

646− put (UI s ((binderTy x, binderTy y,

656+ put (UI s ((binderTy x, binderTy y,

647657 False,

648658 env, err, from, Unify) : f))

649659 return [] -- lift $ tfail err

src/Idris/Core/WHNF.hs+28−23

@@ -1,13 +1,19 @@

1+{-|

2+Module : Idris.Core.WHNF

3+Description : Reduction to Weak Head Normal Form

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE PatternGuards #-}

210{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−

4−-- | Reduction to Weak Head Normal Form

511module Idris.Core.WHNF(whnf, WEnv) where

612

713import Idris.Core.TT

814import Idris.Core.CaseTree

915import Idris.Core.Evaluate hiding (quote)

10−import qualified Idris.Core.Evaluate as Evaluate

16+import qualified Idris.Core.Evaluate as Evaluate

1117

1218import Debug.Trace

1319

@@ -15,7 +21,7 @@ import Debug.Trace

1521-- evaluated in (i.e. it's a thunk)

1622type StackEntry = (Term, WEnv)

1723data WEnv = WEnv Int -- number of free variables

18− [(Term, WEnv)]

24+ [(Term, WEnv)]

1925 deriving Show

2026

2127type Stack = [StackEntry]

@@ -48,14 +54,14 @@ do_whnf :: Context -> WEnv -> Term -> WHNF

4854do_whnf ctxt env tm = eval env [] tm

4955 where

5056 eval :: WEnv -> Stack -> Term -> WHNF

51− eval wenv@(WEnv d env) stk (V i)

57+ eval wenv@(WEnv d env) stk (V i)

5258 | i < length env = let (tm, env') = env !! i in

5359 eval env' stk tm

5460 | otherwise = error "Can't happen: WHNF scope error"

55− eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)

61+ eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)

5662 = eval (WEnv d ((v, wenv) : env)) stk sc

5763 eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)

58− eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)

64+ eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)

5965 = eval (WEnv d ((tm, tenv) : env)) stk sc

6066

6167 eval env stk (P nt n ty) = apply env nt n ty stk

@@ -71,7 +77,7 @@ do_whnf ctxt env tm = eval env [] tm

7177 eval env stk (UType u) = unload (WUType u) stk

7278

7379 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF

74− apply env nt n ty stk

80+ apply env nt n ty stk

7581 = let wp = case nt of

7682 DCon t a u -> WDCon t a u n (ty, env)

7783 TCon t a -> WTCon t a n (ty, env)

@@ -79,12 +85,12 @@ do_whnf ctxt env tm = eval env [] tm

7985 _ -> WPRef n (ty, env)

8086 in

8187 case lookupDefExact n ctxt of

82− Just (CaseOp ci _ _ _ _ cd) ->

88+ Just (CaseOp ci _ _ _ _ cd) ->

8389 let (ns, tree) = cases_compiletime cd in

8490 case evalCase env ns tree stk of

8591 Just w -> w

8692 Nothing -> unload wp stk

87− Just (Operator _ i op) ->

93+ Just (Operator _ i op) ->

8894 if i <= length stk

8995 then case runOp env op (take i stk) (drop i stk) of

9096 Just v -> v

@@ -97,7 +103,7 @@ do_whnf ctxt env tm = eval env [] tm

97103 unload f (a : as) = unload (WApp f a) as

98104

99105 runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF

100− runOp env op stk rest

106+ runOp env op stk rest

101107 = do vals <- mapM tmtoValue stk

102108 case op vals of

103109 Just (VConstant c) -> Just $ unload (WConstant c) rest

@@ -110,14 +116,14 @@ do_whnf ctxt env tm = eval env [] tm

110116 _ -> Nothing

111117

112118 tmtoValue :: (Term, WEnv) -> Maybe Value

113− tmtoValue (tm, tenv)

119+ tmtoValue (tm, tenv)

114120 = case eval tenv [] tm of

115121 WConstant c -> Just (VConstant c)

116122 _ -> let tm' = quoteEnv tenv tm in

117123 Just (toValue ctxt [] tm')

118124

119125 evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF

120− evalCase wenv@(WEnv d env) ns tree args

126+ evalCase wenv@(WEnv d env) ns tree args

121127 | length ns > length args = Nothing

122128 | otherwise = let args' = take (length ns) args

123129 rest = drop (length ns) args in

@@ -125,25 +131,25 @@ do_whnf ctxt env tm = eval env [] tm

125131 let wtm = pToVs (map fst amap) tm

126132 Just $ eval (WEnv d (map snd amap)) rest wtm

127133

128− evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->

134+ evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->

129135 Maybe (Term, [(Name, (Term, WEnv))])

130136 evalTree env amap (STerm tm) = Just (tm, amap)

131137 evalTree env amap (Case _ n alts)

132138 = case lookup n amap of

133− Just (tm, tenv) -> findAlt env amap

139+ Just (tm, tenv) -> findAlt env amap

134140 (deconstruct (eval tenv [] tm) []) alts

135141 _ -> Nothing

136142 evalTree _ _ _ = Nothing

137143

138144 deconstruct :: WHNF -> Stack -> (WHNF, Stack)

139145 deconstruct (WApp f arg) stk = deconstruct f (arg : stk)

140− deconstruct t stk = (t, stk)

146+ deconstruct t stk = (t, stk)

141147

142− findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->

148+ findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->

143149 [CaseAlt] ->

144150 Maybe (Term, [(Name, (Term, WEnv))])

145− findAlt env amap (WDCon tag _ _ _ _, args) alts

146− | Just (ns, sc) <- findTag tag alts

151+ findAlt env amap (WDCon tag _ _ _ _, args) alts

152+ | Just (ns, sc) <- findTag tag alts

147153 = let amap' = updateAmap (zip ns args) amap in

148154 evalTree env amap' sc

149155 | Just sc <- findDefault alts

@@ -159,7 +165,7 @@ do_whnf ctxt env tm = eval env [] tm

159165 findTag i [] = Nothing

160166 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)

161167 findTag i (_ : xs) = findTag i xs

162−

168+

163169 findDefault :: [CaseAlt] -> Maybe SC

164170 findDefault [] = Nothing

165171 findDefault (DefaultCase sc : xs) = Just sc

@@ -182,7 +188,7 @@ do_whnf ctxt env tm = eval env [] tm

182188quote :: WHNF -> Term

183189quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)

184190quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)

185−quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)

191+quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)

186192quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)

187193quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)

188194quote (WConstant c) = Constant c

@@ -195,7 +201,7 @@ quote WImpossible = Impossible

195201quoteEnv :: WEnv -> Term -> Term

196202quoteEnv (WEnv d ws) tm = qe' d ws tm

197203 where

198− qe' d ts (V i)

204+ qe' d ts (V i)

199205 | i < d = V i

200206 | otherwise = let (tm, env) = ts !! (i - d) in

201207 quoteEnv env tm

@@ -206,4 +212,3 @@ quoteEnv (WEnv d ws) tm = qe' d ws tm

206212 qe' d ts (P nt n ty) = P nt n (qe' d ts ty)

207213 qe' d ts (Proj tm i) = Proj (qe' d ts tm) i

208214 qe' d ts tm = tm

209−

src/Idris/Coverage.hs+8−3

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

1−{-# LANGUAGE PatternGuards #-}

2−{-| The coverage and totality checkers for Idris are in this module.

1+{-|

2+Module : Idris.Coverage

3+Description : The coverage and totality checkers for Idris are in this module.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

37-}

8+{-# LANGUAGE PatternGuards #-}

49module Idris.Coverage where

510

611import Idris.Core.TT

@@ -352,7 +357,7 @@ checkPositive mut_ns (cn, ty')

352357 where

353358 args t = [0..length (getArgTys t)-1]

354359

355− cp i (Bind n (Pi _ aty _) sc)

360+ cp i (Bind n (Pi _ aty _) sc)

356361 = posArg i aty && cp i sc

357362 cp i t | (P _ n' _ , args) <- unApply t,

358363 n' `elem` mut_ns = all noRec args

src/Idris/DSL.hs+9−3

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.DSL

3+Description : Code to deal with DSL blocks.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE PatternGuards #-}

210

311module Idris.DSL where

@@ -16,7 +24,7 @@ debindApp :: SyntaxInfo -> PTerm -> PTerm

1624debindApp syn t = debind (dsl_bind (dsl_info syn)) t

1725

1826dslify :: SyntaxInfo -> IState -> PTerm -> PTerm

19−dslify syn i = transform dslifyApp

27+dslify syn i = transform dslifyApp

2028 where

2129 dslifyApp (PApp fc (PRef _ _ f) [a])

2230 | [d] <- lookupCtxt f (idris_dsls i)

@@ -225,5 +233,3 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

225233 bindAll [] tm = tm

226234 bindAll ((n, fc, t) : bs) tm

227235 = PApp fc b [pexp t, pexp (PLam fc n NoFC Placeholder (bindAll bs tm))]

228−

229−

src/Idris/DataOpts.hs+7−2

@@ -1,9 +1,14 @@

1+{-|

2+Module : Idris.DataOpts

3+Description : Optimisations for Idris code i.e. Forcing, detagging and collapsing.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29

310module Idris.DataOpts(applyOpts) where

411

5−-- Forcing, detagging and collapsing

6−

712import Idris.AbsSyntax

813import Idris.AbsSyntaxTree

914import Idris.Core.TT

src/Idris/DeepSeq.hs+11−1

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

1+{-|

2+Module : Idris.DeepSeq

3+Description : Specify how to marshall Idris' IR.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

29

3−module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where

10+module Idris.DeepSeq(

11+ module Idris.DeepSeq

12+ , module Idris.Core.DeepSeq

13+ ) where

414

515import Idris.Core.DeepSeq

616import Idris.Docstrings

src/Idris/Delaborate.hs+30−23

@@ -1,9 +1,17 @@

1+{-|

2+Module : Idris.Delaborate

3+Description : Convert core TT back into high level syntax, primarily for display purposes.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab, pprintDelabTy, pprintErr, resugar) where

4−

5−-- Convert core TT back into high level syntax, primarily for display

6−-- purposes.

10+module Idris.Delaborate (

11+ annName, bugaddr, delab, delab', delabMV, delabSugared

12+ , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab

13+ , pprintDelabTy, pprintErr, resugar

14+ ) where

715

816import Util.Pretty

917

@@ -253,12 +261,12 @@ pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation

253261pprintProv i e ExpectedType = text "Expected type"

254262pprintProv i e InferredVal = text "Inferred value"

255263pprintProv i e GivenVal = text "Given value"

256−pprintProv i e (SourceTerm tm)

257− = text "Type of " <>

264+pprintProv i e (SourceTerm tm)

265+ = text "Type of " <>

258266 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

259267 (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))

260−pprintProv i e (TooManyArgs tm)

261− = text "Is " <>

268+pprintProv i e (TooManyArgs tm)

269+ = text "Is " <>

262270 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

263271 (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))

264272 <> text " applied to too many arguments?"

@@ -277,14 +285,14 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

277285 (x, y) = addImplicitDiffs (delabSugared i x_ns) (delabSugared i y_ns) in

278286 text "Type mismatch between" <> indented (annTm x_ns

279287 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

280− ++ zip nms (repeat False)) x))

288+ ++ zip nms (repeat False)) x))

281289 <> case xprov of

282290 Nothing -> empty

283291 Just t -> text " (" <> pprintProv i sc t <> text ")"

284292 <$>

285293 text "and" <> indented (annTm y_ns

286294 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

287− ++ zip nms (repeat False)) y))

295+ ++ zip nms (repeat False)) y))

288296 <> case yprov of

289297 Nothing -> empty

290298 Just t -> text " (" <> pprintProv i sc t <> text ")"

@@ -301,7 +309,7 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

301309 else empty

302310pprintErr' i (CantConvert x_in y_in env) =

303311 let (x_ns, y_ns, nms) = renameMNs x_in y_in

304− (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

312+ (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

305313 (delabSugared i (flagUnique y_ns)) in

306314 text "Type mismatch between" <>

307315 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

@@ -346,14 +354,14 @@ pprintErr' i (NotInjective p x y) =

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

347355 text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>

348356 annTm y (pprintTerm i (delabSugared i y))

349−pprintErr' i (CantResolve _ c e)

357+pprintErr' i (CantResolve _ c e)

350358 = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)

351359 <>

352360 case e of

353361 Msg "" -> empty

354362 _ -> line <> line <> text "Possible cause:" <>

355363 indented (pprintErr' i e)

356−pprintErr' i (InvalidTCArg n t)

364+pprintErr' i (InvalidTCArg n t)

357365 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "

358366 <> annName n <$>

359367 text "(Implementation arguments must be injective)"

@@ -367,13 +375,13 @@ pprintErr' i (WithFnType ty) =

367375 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))

368376pprintErr' i (CantMatch t) =

369377 text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))

370−pprintErr' i (IncompleteTerm t)

378+pprintErr' i (IncompleteTerm t)

371379 = let missing = getMissing [] [] t in

372380 case missing of

373381 [] -> text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))

374− _ -> align (cat (punctuate (comma <> space)

382+ _ -> align (cat (punctuate (comma <> space)

375383 (map pprintIncomplete (nub $ getMissing [] [] t))))

376− where

384+ where

377385 pprintIncomplete (tm, arg)

378386 | expname arg

379387 = text "Can't infer explicit argument to" <+>

@@ -396,7 +404,7 @@ pprintErr' i (IncompleteTerm t)

396404 getMissing hs env (Bind n (Guess _ _) sc)

397405 = getMissing (n : hs) (n : env) sc

398406 getMissing hs env (Bind n (Let t v) sc)

399− = getMissing hs env t ++

407+ = getMissing hs env t ++

400408 getMissing hs env v ++

401409 getMissing hs (n : env) sc

402410 getMissing hs env (Bind n b sc)

@@ -408,7 +416,7 @@ pprintErr' i (IncompleteTerm t)

408416 getMissingArgs n [] = []

409417 getMissingArgs n (V i : as)

410418 | env!!i `elem` hs = (n, env!!i) : getMissingArgs n as

411− getMissingArgs n (P _ a _ : as)

419+ getMissingArgs n (P _ a _ : as)

412420 | a `elem` hs = (n, a) : getMissingArgs n as

413421 getMissingArgs n (a : as) = getMissing hs env a ++ getMissingArgs n as

414422 getMissing hs env (App _ f a)

@@ -447,11 +455,11 @@ pprintErr' i (ProofSearchFail e) = pprintErr' i e

447455pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))

448456pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

449457pprintErr' i (Elaborating s n ty e) = text "When checking" <+> text s <>

450− annName' n (showqual i n) <>

458+ annName' n (showqual i n) <>

451459 pprintTy ty <$>

452460 pprintErr' i e

453461 where pprintTy Nothing = colon

454− pprintTy (Just ty) = text " with expected type" <>

462+ pprintTy (Just ty) = text " with expected type" <>

455463 indented (annTm ty (pprintTerm i (delabSugared i ty)))

456464 <> line

457465pprintErr' i (ElaboratingArg f x _ e)

@@ -540,12 +548,12 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

540548 where

541549 getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]

542550 getRenames acc [] = return acc

543− getRenames acc (n@(MN i x) : xs) | rpt x xs

551+ getRenames acc (n@(MN i x) : xs) | rpt x xs

544552 = do idx <- get

545553 put (idx + 1)

546554 let x' = sUN (str x ++ show idx)

547555 getRenames ((n, x') : acc) xs

548− getRenames acc (n@(UN x) : xs) | rpt x xs

556+ getRenames acc (n@(UN x) : xs) | rpt x xs

549557 = do idx <- get

550558 put (idx + 1)

551559 let x' = sUN (str x ++ show idx)

@@ -697,4 +705,3 @@ showbasic (MN _ s) = str s

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

698706showbasic (SN s) = show s

699707showbasic n = show n

700−

src/Idris/Directives.hs+7−1

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

1−

1+{-|

2+Module : Idris.Directives

3+Description : Act upon Idris directives.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

28module Idris.Directives(directiveAction) where

39

410import Idris.AbsSyntax

src/Idris/Docs.hs+15−4

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

1+{-|

2+Module : Idris.Docs

3+Description : Data structures and utilities to work with Idris Documentation.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, pprintTypeDoc, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

10+module Idris.Docs (

11+ pprintDocs

12+ , getDocs, pprintConstDocs, pprintTypeDoc

13+ , FunDoc, FunDoc'(..), Docs, Docs'(..)

14+ ) where

415

516import Idris.AbsSyntax

617import Idris.AbsSyntaxTree

@@ -149,7 +160,7 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

149160 vsep (map dumpInstance superclasses)))

150161 where

151162 params' = zip pNames (repeat False)

152−

163+

153164 (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)

154165 instances

155166

@@ -318,7 +329,7 @@ docClass n ci

318329 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

319330 namedInst n@(UN _) = Just n

320331 namedInst _ = Nothing

321−

332+

322333 getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

323334 getDInst _ = Nothing

324335

@@ -380,4 +391,4 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty

380391

381392pprintTypeDoc :: IState -> Doc OutputAnnotation

382393pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>

383− nest 4 (line <> text typeDescription)

394+ nest 4 (line <> text typeDescription)

src/Idris/Docstrings.hs+11−4

@@ -1,10 +1,17 @@

1+{-|

2+Module : Idris.Docstrings

3+Description : Wrapper around Markdown library.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

210{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−

4−-- | Wrapper around Markdown library

511module Idris.Docstrings (

6− Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,

7− overview, containsText, renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring

12+ Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring

13+ , emptyDocstring, nullDocstring, noDocs, overview, containsText

14+ , renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring

815 ) where

916

1017import qualified Cheapskate as C

src/Idris/Elab/AsPat.hs+8−1

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.AsPat

3+Description : Code to elaborate pattern variables.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.Elab.AsPat(desugarAs) where

29

310import Idris.Core.TT

@@ -30,7 +37,7 @@ collectAs (PApp fc t as)

3037 return (PApp fc t as') -- only valid on args

3138-- only for 'ExactlyOne' since it means the alternatives will have the

3239-- same form, so we can assume we only need to extract from the first one

33−collectAs tm@(PAlternative ns (ExactlyOne d) (a : as))

40+collectAs tm@(PAlternative ns (ExactlyOne d) (a : as))

3441 = do a' <- collectAs a

3542 pats <- get

3643 as' <- mapM collectAs as -- just to drop the '@'

src/Idris/Elab/Class.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Class

3+Description : Code to elaborate interfaces.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29{-# OPTIONS_GHC -fwarn-missing-signatures #-}

310module Idris.Elab.Class(elabClass) where

src/Idris/Elab/Clause.hs+10−3

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Clause

3+Description : Code to elaborate clauses.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module Idris.Elab.Clause where

310

@@ -1049,13 +1056,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10491056 getApp [] = Nothing

10501057 currentFn _ tm = tm

10511058

1052− updateApp wtm@(PWithApp fcw tm_in warg) =

1059+ updateApp wtm@(PWithApp fcw tm_in warg) =

10531060 let tm = currentFn fname tm_in in

10541061 case matchClause ist toplhs tm of

10551062 Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))

1056− Right mvars ->

1063+ Right mvars ->

10571064 let ns = map (keepMvar (map fst mvars) fcw) ns_in

1058− ns' = map (keepMvar (map fst mvars) fcw) ns_in'

1065+ ns' = map (keepMvar (map fst mvars) fcw) ns_in'

10591066 wty = lookupTyExact wname (tt_ctxt ist)

10601067 res = substMatches mvars $

10611068 PApp fcw (PRef fcw [] wname)

src/Idris/Elab/Data.hs+8−1

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Data

3+Description : Code to elaborate data structures.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module Idris.Elab.Data(elabData) where

310

@@ -206,7 +213,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

206213 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)

207214 tyIs con t | (P Bound n' _, _) <- unApply t

208215 = if n' /= tn then

209− tclift $ tfail (At fc (Elaborating "constructor " con Nothing

216+ tclift $ tfail (At fc (Elaborating "constructor " con Nothing

210217 (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))

211218 else return ()

212219 tyIs con t | (P _ n' _, _) <- unApply t

src/Idris/Elab/Instance.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Instance

3+Description : Code to elaborate instances.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module Idris.Elab.Instance(elabInstance) where

310

src/Idris/Elab/Provider.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Provider

3+Description : Code to elaborate type providers.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module Idris.Elab.Provider(elabProvider) where

310

src/Idris/Elab/Quasiquote.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Quasiquote

3+Description : Code to elaborate quasiquotations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.Elab.Quasiquote (extractUnquotes) where

29

310import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/Elab/Record.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Record

3+Description : Code to elaborate records.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards, ViewPatterns #-}

29module Idris.Elab.Record(elabRecord) where

310

src/Idris/Elab/Rewrite.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Rewrite

3+Description : Code to elaborate rewrite rules.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards, ViewPatterns #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

310module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where

src/Idris/Elab/RunElab.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.RunElab

3+Description : Code to run the elaborator process.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.Elab.RunElab (elabRunElab) where

29

310import Idris.Elab.Term

src/Idris/Elab/Term.hs+10−3

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Term

3+Description : Code to elaborate terms.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

310module Idris.Elab.Term where

@@ -1664,7 +1671,7 @@ pruneByType env (P _ n _) goalty ist as

16641671 case unApply (getRetTy ty') of

16651672 (V _, _) ->

16661673 isPlausible ist var env n ty

1667− _ -> matching (getRetTy ty') goalty

1674+ _ -> matching (getRetTy ty') goalty

16681675 || isCoercion (getRetTy ty') goalty

16691676-- May be useful to keep for debugging purposes for a bit:

16701677-- let res = matching (getRetTy ty') goalty in

@@ -1698,7 +1705,7 @@ pruneByType env (P _ n _) goalty ist as

16981705 isCoercion rty gty | (P _ r _, _) <- unApply rty

16991706 = not (null (getCoercionsBetween r gty))

17001707 isCoercion _ _ = False

1701−

1708+

17021709 getCoercionsBetween :: Name -> Type -> [Name]

17031710 getCoercionsBetween r goal

17041711 = let cs = getCoercionsTo ist goal in

@@ -1711,7 +1718,7 @@ pruneByType env (P _ n _) goalty ist as

17111718 _ -> [] in

17121719 ps ++ findCoercions t ns

17131720

1714− useR ty =

1721+ useR ty =

17151722 case unApply (getRetTy ty) of

17161723 (P _ t _, _) -> t == r

17171724 _ -> False

src/Idris/Elab/Transform.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Transform

3+Description : Transformations for elaborate terms.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module Idris.Elab.Transform where

310

src/Idris/Elab/Type.hs+11−2

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

1+{-|

2+Module : Idris.Elab.Type

3+Description : Code to elaborate types.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

2−module Idris.Elab.Type (buildType, elabType, elabType',

3− elabPostulate, elabExtern) where

9+module Idris.Elab.Type (

10+ buildType, elabType, elabType'

11+ , elabPostulate, elabExtern

12+ ) where

413

514import Idris.AbsSyntax

615import Idris.ASTUtils

src/Idris/Elab/Utils.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Elab.Utils

3+Description : Elaborator utilities.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29module Idris.Elab.Utils where

310

src/Idris/Elab/Value.hs+11−2

@@ -1,7 +1,16 @@

1+{-|

2+Module : Idris.Elab.Value

3+Description : Code to elaborate values.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,

4− elabExec, elabREPL) where

10+module Idris.Elab.Value(

11+ elabVal, elabValBind, elabDocTerms

12+ , elabExec, elabREPL

13+ ) where

514

615import Idris.AbsSyntax

716import Idris.ASTUtils

src/Idris/ElabDecls.hs+8

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.ElabDecls

3+Description : Code to elaborate declarations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

210 PatternGuards #-}

311

src/Idris/Erasure.hs+8−1

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Erasure

3+Description : Utilities to erase irrelevant stuff.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29

310module Idris.Erasure (performUsageAnalysis, mkFieldName) where

@@ -54,7 +61,7 @@ type DepSet = Map Node (Set Reason)

5461-- "function f uses the argument i".

5562type Cond = Set Node

5663

57−-- ^ Variables carry certain information with them.

64+-- | Variables carry certain information with them.

5865data VarInfo = VI

5966 { viDeps :: DepSet -- ^ dependencies drawn in by the variable

6067 , viFunArg :: Maybe Int -- ^ which function argument this variable came from (defined only for patvars)

src/Idris/ErrReverse.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.ErrReverse

3+Description : Utility to make errors readable using transformations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29

310module Idris.ErrReverse(errReverse) where

src/Idris/Error.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Error

3+Description : Utilities to deal with error reporting.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE DeriveDataTypeable #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

310

src/Idris/Help.hs+8

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.Help

3+Description : Utilities to aid with the REPL's HELP system.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19module Idris.Help (CmdArg(..), extraHelp) where

210

311data CmdArg = ExprArg -- ^ The command takes an expression

src/Idris/IBC.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.IBC

3+Description : Core representations and code to generate IBC files.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE TypeSynonymInstances #-}

29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

310

src/Idris/IdeMode.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.IdeMode

3+Description : Idris' IDE Mode

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

29

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

src/Idris/IdrisDoc.hs+7−2

@@ -1,8 +1,13 @@

1+{-|

2+Module : Idris.IdrisDoc

3+Description : Generation of HTML documentation for Idris code

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29{-# LANGUAGE OverloadedStrings #-}

310{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

4−

5−-- | Generation of HTML documentation for Idris code

611module Idris.IdrisDoc (generateDocs) where

712

813import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),

src/Idris/Imports.hs+11−2

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

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

2− ibcPathNoFallback, installedPackages, pkgIndex) where

1+{-|

2+Module : Idris.Imports

3+Description : Code to handle import declarations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+module Idris.Imports(

9+ IFileType(..), findImport, findInPath, findPkgIndex

10+ , ibcPathNoFallback, installedPackages, pkgIndex

11+ ) where

312

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

514import Data.List (isSuffixOf)

src/Idris/Inliner.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Inliner

3+Description : Idris' Inliner.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29

310module Idris.Inliner(inlineDef, inlineTerm) where

src/Idris/Interactive.hs+13−6

@@ -1,11 +1,18 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-|

2+Module : Idris.Interactive

3+Description : Bits and pieces for editing source files interactively, called from the REPL

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

28

3−module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,

4− addMissing, makeWith, makeCase, doProofSearch,

5− makeLemma) where

9+{-# LANGUAGE PatternGuards #-}

610

7−{- Bits and pieces for editing source files interactively, called from

8− the REPL -}

11+module Idris.Interactive(

12+ caseSplitAt, addClauseFrom, addProofClauseFrom

13+ , addMissing, makeWith, makeCase, doProofSearch

14+ , makeLemma

15+ ) where

916

1017import Idris.Core.TT

1118import Idris.Core.Evaluate

src/Idris/Output.hs+9−1

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.Output

3+Description : Utilities to display Idris' internals and other informtation to the user.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

210

311module Idris.Output where

@@ -99,7 +107,7 @@ iPrintFunTypes bnd n overloads = do ist <- getIState

99107 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

100108 iRenderResult output

101109 where fullName ppo n | length overloads > 1 = prettyName True True bnd n

102− | otherwise = prettyName True (ppopt_impl ppo) bnd n

110+ | otherwise = prettyName True (ppopt_impl ppo) bnd n

103111 ppOverload ppo infixes n tm =

104112 fullName ppo n <+> colon <+> align tm

105113

src/Idris/Parser.hs+8−1

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Parser

3+Description : Idris' parser.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

29{-# OPTIONS_GHC -O0 #-}

310module Idris.Parser(module Idris.Parser,

@@ -797,7 +804,7 @@ openInterface syn =

797804 <?> "open interface declaration"

798805

799806

800−

807+

801808

802809

803810{-| Parses a mutual declaration (for mutually recursive functions)

src/Idris/Parser/Data.hs+16−7

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

1+{-|

2+Module : Idris.Parser.Data

3+Description : Parse Data declarations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

29module Idris.Parser.Data where

310

411import Prelude hiding (pi)

512

613import Text.Trifecta.Delta

7−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

8−import Text.Parser.LookAhead

9−import Text.Parser.Expression

14+import Text.Trifecta hiding ( span, stringLiteral, charLiteral, natural

15+ , symbol, char, string, whiteSpace, Err)

16+

17+import Text.Parser.LookAhead

18+import Text.Parser.Expression

1019import qualified Text.Parser.Token as Tok

1120import qualified Text.Parser.Char as Chr

1221import qualified Text.Parser.Token.Highlight as Hi

@@ -26,11 +35,11 @@ import Control.Applicative

2635import Control.Monad

2736import Control.Monad.State.Strict

2837

29−import Data.Maybe

38+import Data.Maybe

3039import qualified Data.List.Split as Spl

31−import Data.List

32−import Data.Monoid

33−import Data.Char

40+import Data.List

41+import Data.Monoid

42+import Data.Char

3443import qualified Data.HashSet as HS

3544import qualified Data.Text as T

3645import qualified Data.ByteString.UTF8 as UTF8

src/Idris/Parser/Expr.hs+13−5

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

1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}

1+{-|

2+Module : Idris.Parser.Expr

3+Description : Parse Expressions.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds #-}

9+{-# LANGUAGE PatternGuards, TupleSections #-}

210module Idris.Parser.Expr where

311

412import Prelude hiding (pi)

@@ -80,7 +88,7 @@ expr = pi

8088-}

8189opExpr :: SyntaxInfo -> IdrisParser PTerm

8290opExpr syn = do i <- get

83− buildExpressionParser (table (idris_infixes i))

91+ buildExpressionParser (table (idris_infixes i))

8492 (expr' syn)

8593

8694{- | Parses either an internally defined expression or

@@ -955,8 +963,8 @@ rewriteTerm syn = do kw <- reservedFC "rewrite"

955963 fc <- getFC

956964 prf <- expr syn

957965 giving <- optional (do symbol "==>"; expr' syn)

958− using <- optional (do reserved "using"

959− (n, _) <- name

966+ using <- optional (do reserved "using"

967+ (n, _) <- name

960968 return n)

961969 kw' <- reservedFC "in"; sc <- expr syn

962970 highlightP kw AnnKeyword

@@ -1128,7 +1136,7 @@ pi syn =

11281136 st <- static

11291137 explicitPi opts st syn

11301138 <|> try (do lchar '{'; implicitPi opts st syn)

1131− <|> if constraintAllowed syn

1139+ <|> if constraintAllowed syn

11321140 then try (constraintPi opts st syn)

11331141 <|> unboundPi opts st syn

11341142 else unboundPi opts st syn

src/Idris/Parser/Helpers.hs+9−1

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

1−{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, StandaloneDeriving #-}

1+{-|

2+Module : Idris.Parser.Helpers

3+Description : Utilities for Idris' parser.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds #-}

9+{-# LANGUAGE PatternGuards, StandaloneDeriving #-}

210#if !(MIN_VERSION_base(4,8,0))

311{-# LANGUAGE OverlappingInstances #-}

412#endif

src/Idris/Parser/Ops.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Parser.Ops

3+Description : Parser for operators and fixity declarations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

29module Idris.Parser.Ops where

310

src/Idris/PartialEval.hs+12−3

@@ -1,8 +1,17 @@

1+{-|

2+Module : Idris.PartialEval

3+Description : Implementation of a partial evaluator.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards #-}

29

3−module Idris.PartialEval(partial_eval, getSpecApps, specType,

4− mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),

5− pe_app, pe_def, pe_clauses, pe_simple) where

10+module Idris.PartialEval(

11+ partial_eval, getSpecApps, specType

12+ , mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)

13+ , pe_app, pe_def, pe_clauses, pe_simple

14+ ) where

615

716import Idris.AbsSyntax

817import Idris.Delaborate

src/Idris/Primitives.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Primitives

3+Description : Provision of primitive data types.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}

29

310module Idris.Primitives(primitives, Prim(..)) where

src/Idris/ProofSearch.hs+14−1

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

1+{-|

2+Module : Idris.ProofSearch

3+Description : Searches current context for proofs'

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE PatternGuards #-}

210

3−module Idris.ProofSearch(trivial, trivialHoles, proofSearch, resolveTC) where

11+module Idris.ProofSearch(

12+ trivial

13+ , trivialHoles

14+ , proofSearch

15+ , resolveTC

16+ ) where

417

518import Idris.Core.Elaborate hiding (Tactic(..))

619import Idris.Core.TT

src/Idris/Prover.hs+7−1

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

1−

1+{-|

2+Module : Idris.Prover

3+Description : Idris' theorem prover.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

28{-# LANGUAGE PatternGuards #-}

39module Idris.Prover (prover, showProof, showRunElab) where

410

src/Idris/Providers.hs+12−2

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

1+{-|

2+Module : Idris.Providers

3+Description : Idris' 'Type Provider' implementation.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE PatternGuards, DeriveFunctor #-}

2−module Idris.Providers (providerTy, getProvided, Provided(..)) where

9+module Idris.Providers (

10+ providerTy

11+ , getProvided

12+ , Provided(..)

13+ ) where

314

415import Idris.Core.TT

516import Idris.Core.Evaluate

@@ -39,4 +50,3 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

3950 | otherwise = ifail $ "Internal type provider error: result was not " ++

4051 "IO (Provider a), or perhaps missing normalisation." ++

4152 "Term: " ++ take 1000 (show tm)

42−

src/Idris/REPL.hs+14−5

@@ -1,10 +1,19 @@

1+{-|

2+Module : Idris.REPL

3+Description : Entry Point for the Idris REPL and CLI.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

29 PatternGuards, CPP #-}

310

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

5− getPkgREPL, getPkgTest, getPort, getIBCSubDir,

6− idris, idrisMain, loadInputs,

7− opt, runClient, runMain, ver) where

11+module Idris.REPL(

12+ getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc

13+ , getPkgREPL, getPkgTest, getPort, getIBCSubDir

14+ , idris, idrisMain, loadInputs

15+ , opt, runClient, runMain, ver

16+ ) where

817

918import Idris.AbsSyntax

1019import Idris.ASTUtils

@@ -1457,7 +1466,7 @@ showTotalN :: IState -> Name -> Doc OutputAnnotation

14571466showTotalN ist n = case lookupTotal n (tt_ctxt ist) of

14581467 [t] -> showN n <> text ", which is" <+> showTotal t ist

14591468 _ -> empty

1460− where

1469+ where

14611470 ppo = ppOptionIst ist

14621471 showN n = annotate (AnnName n Nothing Nothing Nothing) . text $

14631472 showName (Just ist) [] ppo False n

src/Idris/REPL/Browse.hs+8

@@ -1,3 +1,11 @@

1+{-|

2+Module : Idris.REPL.Browse

3+Description : Browse the current namespace.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}

210

311module Idris.REPL.Browse (namespacesInNS, namesInNS) where

src/Idris/REPL/Parser.hs+13−2

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

1−

2−module Idris.REPL.Parser (parseCmd, help, allHelp, setOptions) where

1+{-|

2+Module : Idris.REPL.Parser

3+Description : Parser for the REPL commands.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+module Idris.REPL.Parser (

9+ parseCmd

10+ , help

11+ , allHelp

12+ , setOptions

13+ ) where

314

415import System.FilePath ((</>))

516import System.Console.ANSI (Color(..))

src/Idris/Reflection.hs+8−3

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

1−{-| Code related to Idris's reflection system. This module contains

2−quoters and unquoters along with some supporting datatypes.

1+{-|

2+Module : Idris.Reflection

3+Description : Code related to Idris's reflection system. This module contains quoters and unquoters along with some supporting datatypes.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

37-}

8+

49{-# LANGUAGE PatternGuards, CPP #-}

510{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}

611module Idris.Reflection where

@@ -900,7 +905,7 @@ reflectErr (NotInjective t1 t2 t3) =

900905 , reflect t2

901906 , reflect t3

902907 ]

903−reflectErr (CantResolve _ t more)

908+reflectErr (CantResolve _ t more)

904909 = raw_apply (Var $ reflErrName "CantResolve") [reflect t, reflectErr more]

905910reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

906911reflectErr (CantResolveAlts ss) =

src/Idris/Transforms.hs+14−4

@@ -1,9 +1,19 @@

1+{-|

2+Module : Idris.Transforms

3+Description : A collection of transformations.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+

19{-# LANGUAGE PatternGuards #-}

210

3−module Idris.Transforms(transformPats,

4− transformPatsWith,

5− applyTransRulesWith,

6− applyTransRules) where

11+module Idris.Transforms(

12+ transformPats

13+ , transformPatsWith

14+ , applyTransRulesWith

15+ , applyTransRules

16+ ) where

717

818import Idris.AbsSyntax

919import Idris.Core.CaseTree

src/Idris/TypeSearch.hs+70−61

@@ -1,36 +1,45 @@

1+{-|

2+Module : Idris.TypeSearch

3+Description : A Hoogle for Idris.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE ScopedTypeVariables #-}

29

310module Idris.TypeSearch (

4− searchByType, searchPred, defaultScoreFunction

5−) where

11+ searchByType

12+ , searchPred

13+ , defaultScoreFunction

14+ ) where

615

716import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))

8−import Control.Arrow (first, second, (&&&), (***))

9−import Control.Monad (when, guard)

10−

11−import Data.List (find, partition, (\\))

12−import Data.Map (Map)

13−import qualified Data.Map as M

14−import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)

15−import Data.Monoid (Monoid (mempty, mappend))

16−import Data.Ord (comparing)

17+import Control.Arrow (first, second, (&&&), (***))

18+import Control.Monad (when, guard)

19+

20+import Data.List (find, partition, (\\))

21+import Data.Map (Map)

22+import qualified Data.Map as M

23+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)

24+import Data.Monoid (Monoid (mempty, mappend))

25+import Data.Ord (comparing)

1726import qualified Data.PriorityQueue.FingerTree as Q

18−import Data.Set (Set)

19−import qualified Data.Set as S

20−import qualified Data.Text as T (pack, isPrefixOf)

21−import Data.Traversable (traverse)

22−

23−import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

24−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,

25− IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

26− implicitAllowed, OutputMode(..), PTerm, toplevel)

27+import Data.Set (Set)

28+import qualified Data.Set as S

29+import qualified Data.Text as T (pack, isPrefixOf)

30+import Data.Traversable (traverse)

31+

32+import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

33+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris

34+ , IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

35+ implicitAllowed, OutputMode(..), PTerm, toplevel)

2736import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

28−import Idris.Core.TT hiding (score)

29−import Idris.Core.Unify (match_unify)

30−import Idris.Delaborate (delabTy)

31−import Idris.Docstrings (noDocs, overview)

32−import Idris.Elab.Type (elabType)

33−import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)

37+import Idris.Core.TT hiding (score)

38+import Idris.Core.Unify (match_unify)

39+import Idris.Delaborate (delabTy)

40+import Idris.Docstrings (noDocs, overview)

41+import Idris.Elab.Type (elabType)

42+import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)

3443import Idris.IBC

3544

3645import Prelude hiding (pred)

@@ -40,9 +49,9 @@ import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

4049searchByType :: [String] -> PTerm -> Idris ()

4150searchByType pkgs pterm = do

4251 i <- getIState -- save original

43− when (not (null pkgs)) $

52+ when (not (null pkgs)) $

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

45−

54+

4655 mapM_ loadPkgIndex pkgs

4756 pterm' <- addUsingConstraints syn emptyFC pterm

4857 pterm'' <- implicit toplevel syn name pterm'

@@ -67,9 +76,9 @@ searchByType pkgs pterm = do

6776 name = sMN 0 "searchType" -- name

6877

6978-- | Conduct a type-directed search using a given match predicate

70−searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])

79+searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])

7180 -> IState -> Type -> [(Name, a)]

72−searchUsing pred istate ty = pred istate nty . concat . M.elems $

81+searchUsing pred istate ty = pred istate nty . concat . M.elems $

7382 M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)

7483 where

7584 nty = normaliseC ctxt [] ty

@@ -81,7 +90,7 @@ searchUsing pred istate ty = pred istate nty . concat . M.elems $

8190 special :: Name -> Bool

8291 special (NS n _) = special n

8392 special (SN _) = True

84− special (UN n) = T.pack "default#" `T.isPrefixOf` n

93+ special (UN n) = T.pack "default#" `T.isPrefixOf` n

8594 || n `elem` map T.pack ["believe_me", "really_believe_me"]

8695 special _ = False

8796

@@ -117,10 +126,10 @@ reverseDag xs = map f xs where

117126

118127-- run vToP first!

119128-- | Compute a directed acyclic graph corresponding to the

120−-- arguments of a function.

129+-- arguments of a function.

121130-- returns [(the name and type of the bound variable

122131-- the names in the type of the bound variable)]

123−computeDagP :: Ord n

132+computeDagP :: Ord n

124133 => (TT n -> Bool) -- ^ filter to remove some arguments

125134 -> TT n

126135 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)

@@ -196,7 +205,7 @@ displayScore score = case both noMods (asymMods score) of

196205 Sided True False -> annotated LT "<" -- found type is more general than searched type

197206 Sided False True -> annotated GT ">" -- searched type is more general than found type

198207 Sided False False -> text "_"

199− where

208+ where

200209 annotated ordr = annotate (AnnSearchResult ordr) . text

201210 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0

202211

@@ -208,19 +217,19 @@ scoreCriterion (Score _ _ amods) = not

208217 ( sided (&&) (both ((> 0) . argApp) amods)

209218 || sided (+) (both argApp amods) > 4

210219 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)

211− )

220+ )

212221

213222-- | Convert a 'Score' to an 'Int' to provide an order for search results.

214223-- Lower scores are better.

215224defaultScoreFunction :: Score -> Int

216−defaultScoreFunction (Score trans eqFlip amods) =

225+defaultScoreFunction (Score trans eqFlip amods) =

217226 trans + eqFlip + linearPenalty + upAndDowncastPenalty

218227 where

219228 -- prefer finding a more general type to a less general type

220− linearPenalty = (\(Sided l r) -> 3 * l + r)

229+ linearPenalty = (\(Sided l r) -> 3 * l + r)

221230 (both (\(Mods app tcApp tcIntro) -> 3 * app + 4 * tcApp + 2 * tcIntro) amods)

222231 -- it's very bad to have *both* upcasting and downcasting

223− upAndDowncastPenalty = 100 *

232+ upAndDowncastPenalty = 100 *

224233 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)

225234

226235instance Ord Score where

@@ -237,7 +246,7 @@ instance Monoid AsymMods where

237246

238247instance Monoid Score where

239248 mempty = Score 0 0 mempty

240− (Score t e mods) `mappend` (Score t' e' mods') = Score (t + t') (e + e') (mods `mappend` mods')

249+ (Score t e mods) `mappend` (Score t' e' mods') = Score (t + t') (e + e') (mods `mappend` mods')

241250

242251-- | A directed acyclic graph representing the arguments to a function

243252-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)

@@ -311,7 +320,7 @@ flipEqualities t = case t of

311320 [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]

312321 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))

313322 <$> traverse flipEqualities binder <*> flipEqualities sc

314− App _ f x -> (\(i, f') (j, x') -> (i + j, app f' x'))

323+ App _ f x -> (\(i, f') (j, x') -> (i + j, app f' x'))

315324 <$> flipEqualities f <*> flipEqualities x

316325 t' -> [(0, t')]

317326 where app = App Complete

@@ -329,13 +338,13 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

329338 where

330339 ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))

331340 <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2

332− flipEqualitiesDag dag = case dag of

341+ flipEqualitiesDag dag = case dag of

333342 [] -> [(0, [])]

334− ((n, ty), (pos, deps)) : xs ->

343+ ((n, ty), (pos, deps)) : xs ->

335344 (\(i, ty') (j, xs') -> (i + j , ((n, ty'), (pos, deps)) : xs'))

336345 <$> flipEqualities ty <*> flipEqualitiesDag xs

337346 startStates (numEqFlips, sndDag, sndRetTy) = do

338− state <- unifyQueue (State startingHoles

347+ state <- unifyQueue (State startingHoles

339348 (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))

340349 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]

341350 return (score state, state)

@@ -346,7 +355,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

346355 usedns = map fst startingHoles

347356 startingHoles = argNames1 ++ argNames2

348357

349− startingTypes = [(retTy1, retTy2)]

358+ startingTypes = [(retTy1, retTy2)]

350359

351360

352361 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

@@ -372,14 +381,14 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

372381 (dag1, typeClassArgs1, retTy1) = makeDag type1

373382 argNames1 = map fst dag1

374383 makeDag :: Type -> (ArgsDAG, Classes, Type)

375− makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .

384+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .

376385 computeDagP (isTypeClassArg classInfo) . vToP . unLazy

377386 first3 f (a,b,c) = (f a, b, c)

378−

387+

379388 -- update our state with the unification resolutions

380389 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])

381390 resolveUnis [] state = Just (state, [])

382− resolveUnis ((name, term@(P Bound name2 _)) : xs)

391+ resolveUnis ((name, term@(P Bound name2 _)) : xs)

383392 state | isJust findArgs = do

384393 ((ty1, ix1), (ty2, ix2)) <- findArgs

385394

@@ -408,7 +417,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

408417 -- due to injectivity

409418 matchedVarMap = usedVars term

410419 bothT f (x, y) = (f x, f y)

411− (injUsedVars, notInjUsedVars) = bothT M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst hs) $ M.map snd matchedVarMap

420+ (injUsedVars, notInjUsedVars) = bothT M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst hs) $ M.map snd matchedVarMap

412421 varsInTy = injUsedVars ++ notInjUsedVars

413422 toDelete = name : varsInTy

414423 deleteMany = foldr (.) id (map deleteName toDelete)

@@ -417,7 +426,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

417426

418427 addScore additions theState = theState { score = let s = score theState in

419428 s { asymMods = asymMods s `mappend` additions } }

420− state' = state { holes = filter (not . (`elem` toDelete) . fst) hs

429+ state' = state { holes = filter (not . (`elem` toDelete) . fst) hs

421430 , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }

422431 nextStep = resolveUnis xs state'

423432

@@ -427,8 +436,8 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

427436 unifyQueue state [] = return state

428437 unifyQueue state ((ty1, ty2) : queue) = do

429438 --trace ("go: \n" ++ show state) True `seq` return ()

430− res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]

431− (ty1, Nothing)

439+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]

440+ (ty1, Nothing)

432441 (ty2, Nothing) [] (map fst $ holes state) []

433442 (state', queueAdditions) <- resolveUnis res state

434443 guard $ scoreCriterion (score state')

@@ -453,7 +462,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

453462 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)

454463 nextStepsQueue queue = do

455464 ((nextScore, next), rest) <- Q.minViewWithKey queue

456− Just $ if isFinal next

465+ Just $ if isFinal next

457466 then Right nextScore

458467 else let additions = if scoreCriterion nextScore

459468 then Q.fromList [ (score state, state) | state <- nextSteps next ]

@@ -469,19 +478,19 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

469478 nextSteps :: State -> [State]

470479

471480 -- Stage 3 - match typeclasses

472− nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =

481+ nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =

473482 if null results3 then results4 else results3

474483 where

475484 -- try to match a typeclass argument from the left with a typeclass argument from the right

476485 results3 =

477− catMaybes [ unifyQueue (State []

486+ catMaybes [ unifyQueue (State []

478487 (Sided ([], deleteFromArgList n1 c1)

479488 ([], map (second subst2for1) (deleteFromArgList n2 c2)))

480− scoreAcc usedns) [(ty1, ty2)]

489+ scoreAcc usedns) [(ty1, ty2)]

481490 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

482491

483492 -- try to hunt match a typeclass constraint by replacing it with an instance

484− results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)

493+ results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)

485494 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))

486495 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))

487496 | sds <- allMods ]

@@ -512,10 +521,10 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

512521 canBeFirst = map fst . filter (S.null . snd . snd)

513522

514523 -- try to match an argument from the left with an argument from the right

515− results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) hs)

516− (Sided (deleteFromDag n1 dagL, c1)

524+ results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) hs)

525+ (Sided (deleteFromDag n1 dagL, c1)

517526 (inArgTys subst2for1 $ deleteFromDag n2 dagR, map (second subst2for1) c2))

518− scoreAcc usedns) [(ty1, ty2)]

527+ scoreAcc usedns) [(ty1, ty2)]

519528 | (n1, ty1) <- canBeFirst dagL, (n2, ty2) <- canBeFirst dagR

520529 , let subst2for1 = psubst n2 (P Bound n1 ty1)]

521530

@@ -523,7 +532,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

523532

524533 -- Stage 2 - simply introduce a subset of the typeclasses

525534 -- we've finished, so take some classes

526− takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =

535+ takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =

527536 map statesFromMods . prod $ both (classMods . snd) unresolved

528537 where

529538 swap (Sided l r) = Sided r l

@@ -532,7 +541,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

532541 mods = swap (both snd sides) in

533542 State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns

534543 classMods :: Classes -> [(Classes, AsymMods)]

535− classMods cs = let lcs = length cs in

544+ classMods cs = let lcs = length cs in

536545 [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]

537546 prod :: Sided [a] -> [Sided a]

538547 prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]

src/Idris/Unlit.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.Unlit

3+Description : Turn literate programs into normal programs.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.Unlit(unlit) where

29

310import Idris.Core.TT

src/Idris/WhoCalls.hs+8−1

@@ -1,3 +1,10 @@

1+{-|

2+Module : Idris.WhoCalls

3+Description : Find function callers and callees.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Idris.WhoCalls (whoCalls, callsWho) where

29

310import Idris.AbsSyntax

@@ -77,7 +84,7 @@ findOccurs :: Name -> Idris [Name]

7784findOccurs n = do ctxt <- getContext

7885 -- A definition calls a function if the function is in the type or RHS of the definition

7986 let defs = (map fst . filter (\(n', def) -> n /= n' && occursDef n def) . ctxtAlist) ctxt

80− -- A datatype calls its

87+ -- A datatype calls its

8188 return defs

8289

8390whoCalls :: Name -> Idris [(Name, [Name])]

src/Pkg/PParser.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Pkg.PParser

3+Description : `iPKG` file parser and package description information.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE CPP, ConstraintKinds #-}

29#if !(MIN_VERSION_base(4,8,0))

310{-# LANGUAGE OverlappingInstances #-}

src/Pkg/Package.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Pkg.Package

3+Description : Functionality for working with Idris packages.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE CPP #-}

29module Pkg.Package where

310

src/Util/DynamicLinker.hs+12−5

@@ -1,7 +1,16 @@

1−-- | Platform-specific dynamic linking support. Add new platforms to this file

2−-- through conditional compilation.

1+{-|

2+Module : Util.DynamicLinker

3+Description : Platform-specific dynamic linking support. Add new platforms to this file through conditional compilation.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

38{-# LANGUAGE ExistentialQuantification, CPP #-}

4−module Util.DynamicLinker (ForeignFun(..), DynamicLib(..), tryLoadLib, tryLoadFn) where

9+module Util.DynamicLinker ( ForeignFun(..)

10+ , DynamicLib(..)

11+ , tryLoadLib

12+ , tryLoadFn

13+ ) where

514

615#ifdef IDRIS_FFI

716import Foreign.LibFFI

@@ -110,5 +119,3 @@ tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

110119tryLoadFn fn lib = do putStrLn $ "WARNING: Cannot load '" ++ fn ++ "' at compile time because Idris was compiled without libffi support."

111120 return Nothing

112121#endif

113−

114−

src/Util/Net.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Util.Net

3+Description : Utilities for Network IO.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where

29

310import Network hiding (socketPort)

src/Util/Pretty.hs+12−6

@@ -1,8 +1,16 @@

1+{-|

2+Module : Util.Pretty

3+Description : Utilities for Pretty Printing.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Util.Pretty (

2− module Text.PrettyPrint.Annotated.Leijen,

3− Sized(..), nestingSize,

4− Pretty(..)

5−) where

9+ module Text.PrettyPrint.Annotated.Leijen

10+ , Sized(..)

11+ , nestingSize

12+ , Pretty(..)

13+ ) where

614

715--import Text.PrettyPrint.HughesPJ

816import Text.PrettyPrint.Annotated.Leijen

@@ -22,5 +30,3 @@ nestingSize = 1

2230

2331class Pretty a ty where

2432 pretty :: a -> Doc ty

25−

26−

src/Util/ScreenSize.hs+7

@@ -1,3 +1,10 @@

1+{-|

2+Module : Util.ScreenSize

3+Description : Utilities for getting screen width.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18module Util.ScreenSize(getScreenWidth) where

29

310import System.Console.Terminal.Size (size, width)

src/Util/System.hs+18−4

@@ -1,8 +1,22 @@

1+{-|

2+Module : Util.System

3+Description : Utilities for interacting with the system.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

18{-# LANGUAGE CPP, ForeignFunctionInterface #-}

2−module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,

3− writeSource, writeSourceText, readSource,

4− setupBundledCC, isATTY) where

5−-- System helper functions.

9+module Util.System( tempfile

10+ , withTempdir

11+ , rmFile

12+ , catchIO

13+ , isWindows

14+ , writeSource

15+ , writeSourceText

16+ , readSource

17+ , setupBundledCC

18+ , isATTY

19+ ) where

620

721import Control.Exception as CE

822import Control.Monad (when)