git.iko.soy/Idris-dev
on master help sign in
Added documentation for modules.
0896073Jan de Muijnck-Hughes
src/IRTS/BCImp.hs+7−3
compare with master
unifiedsplit
@@ -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+-}
1module IRTS.BCImp where
8module IRTS.BCImp where
2
9
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−
6import IRTS.Lang
10import IRTS.Lang
7import IRTS.Simplified
11import IRTS.Simplified
8import Idris.Core.TT
12import Idris.Core.TT
src/IRTS/Bytecode.hs+37−35
@@ -1,15 +1,11 @@
1+{-|
1−module IRTS.Bytecode where
2+Module : IRTS.Bytecode
3+Description : Bytecode for a stack based VM (e.g. for generating C code with an accurate hand written GC)
2
4
3−-- Bytecode for a stack based VM (e.g. for generating C code with an accurate
5+Copyright :
4−-- hand written GC)
6+License : BSD3
7+Maintainer : The Idris Community.
5
8
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:
13
9
14BASE: Current stack frame's base
10BASE: Current stack frame's base
15TOP: Top of stack
11TOP: Top of stack
@@ -22,27 +18,35 @@ RVal is a register in which computed values (essentially, what a function
22returns) are stored.
18returns) are stored.
23
19
24-}
20-}
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
25
29
26data Reg = RVal | L Int | T Int | Tmp
30data Reg = RVal | L Int | T Int | Tmp
27 deriving (Show, Eq)
31 deriving (Show, Eq)
28
32
29−data BC =
33+data BC =
30− -- reg1 = reg2
34+ -- | reg1 = reg2
31 ASSIGN Reg Reg
35 ASSIGN Reg Reg
32
36
33− -- reg = const
37+ -- | reg = const
34 | ASSIGNCONST Reg Const
38 | ASSIGNCONST Reg Const
35
39
36− -- reg1 = reg2 (same as assign, it seems)
40+ -- | reg1 = reg2 (same as assign, it seems)
37 | UPDATE Reg Reg
41 | UPDATE Reg Reg
38
42
39− -- reg = constructor, where constructor consists of a tag and
43+ -- | reg = constructor, where constructor consists of a tag and
40 -- values from registers, e.g. (cons tag args)
44 -- values from registers, e.g. (cons tag args)
41 -- the 'Maybe Reg', if set, is a register which can be overwritten
45 -- the 'Maybe Reg', if set, is a register which can be overwritten
42 -- (i.e. safe for mutable update), though this can be ignored
46 -- (i.e. safe for mutable update), though this can be ignored
43 | MKCON Reg (Maybe Reg) Int [Reg]
47 | MKCON Reg (Maybe Reg) Int [Reg]
44
48
45− -- Matching on value of reg: usually (but not always) there are
49+ -- | Matching on value of reg: usually (but not always) there are
46 -- constructors, hence "Int" for patterns (that's a tag on which
50 -- constructors, hence "Int" for patterns (that's a tag on which
47 -- we should match), and the following [BC] is just a list of
51 -- we should match), and the following [BC] is just a list of
48 -- instructions for the corresponding case. The last argument is
52 -- instructions for the corresponding case. The last argument is
@@ -53,57 +57,57 @@ data BC =
53 | CASE Bool
57 | CASE Bool
54 Reg [(Int, [BC])] (Maybe [BC])
58 Reg [(Int, [BC])] (Maybe [BC])
55
59
56− -- get a value from register, which should be a constructor, and
60+ -- | get a value from register, which should be a constructor, and
57 -- put its arguments into the stack, starting from (base + int1)
61 -- put its arguments into the stack, starting from (base + int1)
58 -- and onwards; second Int provides arity
62 -- and onwards; second Int provides arity
59 | PROJECT Reg Int Int
63 | PROJECT Reg Int Int
60
64
61− -- probably not used
65+ -- | probably not used
62 | PROJECTINTO Reg Reg Int -- project argument from one reg into another
66 | PROJECTINTO Reg Reg Int -- project argument from one reg into another
63
67
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
65 | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])
69 | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])
66
70
67− -- just call a function, passing MYOLDBASE (see below) to it
71+ -- | just call a function, passing MYOLDBASE (see below) to it
68 | CALL Name
72 | CALL Name
69
73
70− -- same, perhaps exists just for TCO
74+ -- | same, perhaps exists just for TCO
71 | TAILCALL Name
75 | TAILCALL Name
72
76
73− -- set reg to (apply string args),
77+ -- | set reg to (apply string args),
74 | FOREIGNCALL Reg FDesc FDesc [(FDesc, Reg)]
78 | FOREIGNCALL Reg FDesc FDesc [(FDesc, Reg)]
75
79
76− -- move this number of elements from TOP to BASE
80+ -- | move this number of elements from TOP to BASE
77 | SLIDE Int
81 | SLIDE Int
78
82
79− -- set BASE = OLDBASE
83+ -- | set BASE = OLDBASE
80 | REBASE
84 | REBASE
81
85
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
83 -- necessary)
87 -- necessary)
84 | RESERVE Int
88 | RESERVE Int
85
89
86− -- move the top of stack up
90+ -- | move the top of stack up
87 | ADDTOP Int
91 | ADDTOP Int
88
92
89− -- set TOP = BASE + n
93+ -- | set TOP = BASE + n
90 | TOPBASE Int
94 | TOPBASE Int
91
95
92− -- set BASE = TOP + n
96+ -- | set BASE = TOP + n
93 | BASETOP Int
97 | BASETOP Int
94
98
95− -- set MYOLDBASE = BASE, where MYOLDBASE is a function-local
99+ -- | set MYOLDBASE = BASE, where MYOLDBASE is a function-local
96 -- variable, set to OLDBASE by default, and passed on function
100 -- variable, set to OLDBASE by default, and passed on function
97 -- call to called functions as their OLDBASE
101 -- call to called functions as their OLDBASE
98 | STOREOLD
102 | STOREOLD
99
103
100− -- reg = apply primitive_function args
104+ -- | reg = apply primitive_function args
101 | OP Reg PrimFn [Reg]
105 | OP Reg PrimFn [Reg]
102
106
103− -- clear reg
107+ -- | clear reg
104 | NULL Reg
108 | NULL Reg
105
109
106− -- throw an error
110+ -- | throw an error
107 | ERROR String
111 | ERROR String
108 deriving Show
112 deriving Show
109
113
@@ -138,7 +142,7 @@ bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r
138bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]
142bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]
139 ++ clean r
143 ++ clean r
140-- bc reg (SUpdate x sc) r = bc reg sc r -- can't update, just do it
144-- 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
142 = MKCON reg (getAllocLoc atloc) i (map getL vs) : clean r
146 = MKCON reg (getAllocLoc atloc) i (map getL vs) : clean r
143 where getL (Loc x) = L x
147 where getL (Loc x) = L x
144 getAllocLoc (Just (Loc x)) = Just (L x)
148 getAllocLoc (Just (Loc x)) = Just (L x)
@@ -184,5 +188,3 @@ constAlt l reg r _ = Nothing
184defaultAlt reg [] r = Nothing
188defaultAlt reg [] r = Nothing
185defaultAlt reg (SDefaultCase e : _) r = Just (bc reg e r)
189defaultAlt reg (SDefaultCase e : _) r = Just (bc reg e r)
186defaultAlt reg (_ : xs) r = defaultAlt reg xs r
190defaultAlt 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+-}
1module IRTS.CodegenC (codegenC) where
8module IRTS.CodegenC (codegenC) where
2
9
3import Idris.AbsSyntax
10import Idris.AbsSyntax
@@ -41,17 +48,17 @@ codegenC ci = do codegenC' (simpleDecls ci)
41 where mkLib l = "-l" ++ l
48 where mkLib l = "-l" ++ l
42 incdir i = "-I" ++ i
49 incdir i = "-I" ++ i
43
50
44−codegenC' :: [(Name, SDecl)] ->
51+codegenC' :: [(Name, SDecl)]
45− String -> -- output file name
52+ -> String -- ^ output file name
46− OutputType -> -- generate executable if True, only .o if False
53+ -> OutputType -- ^ generate executable if True, only .o if False
47− [FilePath] -> -- include files
54+ -> [FilePath] -- ^ include files
48− [String] -> -- extra object files
55+ -> [String] -- ^ extra object files
49− [String] -> -- extra compiler flags (libraries)
56+ -> [String] -- ^ extra compiler flags (libraries)
50− [String] -> -- extra compiler flags (anything)
57+ -> [String] -- ^ extra compiler flags (anything)
51− [ExportIFace] ->
58+ -> [ExportIFace]
52− Bool -> -- interfaces too (so make a .o instead)
59+ -> Bool -- ^ interfaces too (so make a .o instead)
53− DbgLevel ->
60+ -> DbgLevel
54− IO ()
61+ -> IO ()
55codegenC' defs out exec incs objs libs flags exports iface dbg
62codegenC' defs out exec incs objs libs flags exports iface dbg
56 = do -- print defs
63 = do -- print defs
57 let bc = map toBC defs
64 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+-}
1module IRTS.CodegenCommon where
8module IRTS.CodegenCommon where
2
9
3import Idris.Core.TT
10import Idris.Core.TT
@@ -7,25 +14,28 @@ import IRTS.Defunctionalise
7data DbgLevel = NONE | DEBUG | TRACE deriving Eq
14data DbgLevel = NONE | DEBUG | TRACE deriving Eq
8data OutputType = Raw | Object | Executable deriving (Eq, Show)
15data OutputType = Raw | Object | Executable deriving (Eq, Show)
9
16
10−-- Everything which might be needed in a code generator - a CG can choose which
17+-- | Everything which might be needed in a code generator.
18+--
19+-- A CG can choose which level of Decls to generate code from
11−-- level of Decls to generate code from (simplified, defunctionalised or merely
20+-- (simplified, defunctionalised or merely lambda lifted) and has
12−-- lambda lifted) and has access to the list of object files, libraries, etc.
21+-- access to the list of object files, libraries, etc.
13
22
14−data CodegenInfo = CodegenInfo { outputFile :: String,
23+data CodegenInfo = CodegenInfo {
24+ outputFile :: String
15− outputType :: OutputType,
25+ , outputType :: OutputType
16− targetTriple :: String,
26+ , targetTriple :: String
17− targetCPU :: String,
27+ , targetCPU :: String
18− includes :: [FilePath],
28+ , includes :: [FilePath]
19− importDirs :: [FilePath],
29+ , importDirs :: [FilePath]
20− compileObjs :: [String],
30+ , compileObjs :: [String]
21− compileLibs :: [String],
31+ , compileLibs :: [String]
22− compilerFlags :: [String],
32+ , compilerFlags :: [String]
23− debugLevel :: DbgLevel,
33+ , debugLevel :: DbgLevel
24− simpleDecls :: [(Name, SDecl)],
34+ , simpleDecls :: [(Name, SDecl)]
25− defunDecls :: [(Name, DDecl)],
35+ , defunDecls :: [(Name, DDecl)]
26− liftDecls :: [(Name, LDecl)],
36+ , liftDecls :: [(Name, LDecl)]
27− interfaces :: Bool,
37+ , interfaces :: Bool
28− exportDecls :: [ExportIFace]
38+ , exportDecls :: [ExportIFace]
29− }
39+ }
30
40
31type CodeGenerator = CodegenInfo -> IO ()
41type 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2{-# LANGUAGE OverloadedStrings #-}
9{-# LANGUAGE OverloadedStrings #-}
3−module IRTS.CodegenJavaScript (codegenJavaScript, codegenNode, JSTarget(..)) where
10+module IRTS.CodegenJavaScript (codegenJavaScript
11+ , codegenNode
12+ , JSTarget(..)
13+ ) where
4
14
5import IRTS.JavaScript.AST
15import IRTS.JavaScript.AST
6
16
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+-}
1{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
8{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
2
9
3module IRTS.Compiler(compile, generate) where
10module IRTS.Compiler(compile, generate) where
@@ -32,13 +39,15 @@ import Prelude hiding (id, (.))
32
39
33import Control.Applicative
40import Control.Applicative
34import Control.Monad.State
41import Control.Monad.State
42+
35−import Data.Maybe
43+import Data.Maybe
36−import Data.List
44+import Data.List
37−import Data.Ord
45+import Data.Ord
38−import Data.IntSet (IntSet)
46+import Data.IntSet (IntSet)
39−import qualified Data.IntSet as IS
47+import qualified Data.IntSet as IS
40−import qualified Data.Map as M
48+import qualified Data.Map as M
41−import qualified Data.Set as S
49+import qualified Data.Set as S
50+
42import System.Process
51import System.Process
43import System.IO
52import System.IO
44import System.Exit
53import 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+-}
1{-# LANGUAGE PatternGuards #-}
22{-# LANGUAGE PatternGuards #-}
2−
3−module IRTS.Defunctionalise(module IRTS.Defunctionalise,
23+module IRTS.Defunctionalise(module IRTS.Defunctionalise
4− module IRTS.Lang) where
24+ , module IRTS.Lang
25+ ) where
5
26
6import IRTS.Lang
27import IRTS.Lang
7import Idris.Core.TT
28import Idris.Core.TT
@@ -61,19 +82,6 @@ getFn xs = mapMaybe fnData xs
61 where fnData (n, LFun _ _ args _) = Just (n, length args)
82 where fnData (n, LFun _ _ args _) = Just (n, length args)
62 fnData _ = Nothing
83 fnData _ = Nothing
63
84
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−
77addApps :: LDefs -> (Name, LDecl) -> State ([Name], [(Name, Int)]) (Name, DDecl)
85addApps :: LDefs -> (Name, LDecl) -> State ([Name], [(Name, Int)]) (Name, DDecl)
78addApps defs o@(n, LConstructor _ t a)
86addApps defs o@(n, LConstructor _ t a)
79 = return (n, DConstructor n t a)
87 = return (n, DConstructor n t a)
@@ -111,7 +119,7 @@ addApps defs (n, LFun _ _ args e)
111 alts' <- mapM (aaAlt env) alts
119 alts' <- mapM (aaAlt env) alts
112 return $ DCase up e' alts'
120 return $ DCase up e' alts'
113 aa env (LConst c) = return $ DConst c
121 aa env (LConst c) = return $ DConst c
114− aa env (LForeign t n args)
122+ aa env (LForeign t n args)
115 = do args' <- mapM (aaF env) args
123 = do args' <- mapM (aaF env) args
116 return $ DForeign t n args'
124 return $ DForeign t n args'
117 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)
125 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)
@@ -133,7 +141,7 @@ addApps defs (n, LFun _ _ args e)
133 = return $ DApp tc n args
141 = return $ DApp tc n args
134 | length args < ar
142 | length args < ar
135 = do (ens, ans) <- get
143 = do (ens, ans) <- get
136− let alln = map (\x -> (n, x)) [length args .. ar]
144+ let alln = map (\x -> (n, x)) [length args .. ar]
137 put (ens, alln ++ ans)
145 put (ens, alln ++ ans)
138 return $ DApp tc (mkUnderCon n (ar - length args)) args
146 return $ DApp tc (mkUnderCon n (ar - length args)) args
139 | length args > ar
147 | length args > ar
@@ -146,14 +154,14 @@ addApps defs (n, LFun _ _ args e)
146 return $ DApp False (mkFnCon n) args
154 return $ DApp False (mkFnCon n) args
147 | length args < ar
155 | length args < ar
148 = do (ens, ans) <- get
156 = do (ens, ans) <- get
149− let alln = map (\x -> (n, x)) [length args .. ar]
157+ let alln = map (\x -> (n, x)) [length args .. ar]
150 put (ens, alln ++ ans)
158 put (ens, alln ++ ans)
151 return $ DApp False (mkUnderCon n (ar - length args)) args
159 return $ DApp False (mkUnderCon n (ar - length args)) args
152 | length args > ar
160 | length args > ar
153 = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)
161 = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)
154
162
155 chainAPPLY f [] = f
163 chainAPPLY f [] = f
156−-- chainAPPLY f (a : b : as)
164+-- chainAPPLY f (a : b : as)
157-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as
165-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as
158 chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as
166 chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as
159
167
@@ -223,7 +231,7 @@ mkApplyCase fname n ar
223 (DApp False (mkUnderCon fname (ar - (n + 1)))
231 (DApp False (mkUnderCon fname (ar - (n + 1)))
224 (map (DV . Glob) (take n (genArgs 0) ++
232 (map (DV . Glob) (take n (genArgs 0) ++
225 [sMN 0 "arg"])))))
233 [sMN 0 "arg"])))))
226− :
234+ :
227 if (ar - (n + 2) >=0 )
235 if (ar - (n + 2) >=0 )
228 then (nm, n, Apply2Case (DConCase (-1) nm (take n (genArgs 0))
236 then (nm, n, Apply2Case (DConCase (-1) nm (take n (genArgs 0))
229 (DApp False (mkUnderCon fname (ar - (n + 2)))
237 (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",
263 mkBigCase (sMN 0 "APPLY") 256
271 mkBigCase (sMN 0 "APPLY") 256
264 (DV (Glob (sMN 0 "fn")))
272 (DV (Glob (sMN 0 "fn")))
265 (cases ++
273 (cases ++
266− [DDefaultCase
274+ [DDefaultCase
267 (DApp False (sMN 0 "APPLY")
275 (DApp False (sMN 0 "APPLY")
268 [DApp False (sMN 0 "APPLY")
276 [DApp False (sMN 0 "APPLY")
269 [DV (Glob (sMN 0 "fn")),
277 [DV (Glob (sMN 0 "fn")),
@@ -320,9 +328,8 @@ instance Show DExp where
320 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e
328 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e
321 showAlt env (DDefaultCase e) = "_ => " ++ show' env e
329 showAlt env (DDefaultCase e) = "_ => " ++ show' env e
322
330
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
324-- 'max' branches
332-- 'max' branches
325−
326mkBigCase cn max arg branches
333mkBigCase cn max arg branches
327 | length branches <= max = DChkCase arg branches
334 | length branches <= max = DChkCase arg branches
328 | otherwise = -- DChkCase arg branches -- until I think of something...
335 | otherwise = -- DChkCase arg branches -- until I think of something...
@@ -368,5 +375,3 @@ dumpDefuns ds = showSep "\n" $ map showDef (toAlist ds)
368 = show fn ++ "(" ++ showSep ", " (map show args) ++ ") = \n\t" ++
375 = show fn ++ "(" ++ showSep ", " (map show args) ++ ") = \n\t" ++
369 show exp ++ "\n"
376 show exp ++ "\n"
370 showDef (x, DConstructor n t a) = "Constructor " ++ show n ++ " " ++ show t
377 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+-}
1module IRTS.DumpBC where
8module IRTS.DumpBC where
2
9
3import IRTS.Lang
10import 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module IRTS.Exports(findExports, getExpNames) where
9module IRTS.Exports(findExports, getExpNames) where
3
10
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+-}
1module IRTS.Inliner where
8module IRTS.Inliner where
2
9
3import Idris.Core.TT
10import Idris.Core.TT
@@ -19,4 +26,3 @@ inl ds d = d
19evalD _ e = ev e
26evalD _ e = ev e
20 where
27 where
21 ev e = Just e
28 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2{-# LANGUAGE OverloadedStrings #-}
9{-# LANGUAGE OverloadedStrings #-}
3module IRTS.JavaScript.AST where
10module 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+-}
1{-# LANGUAGE PatternGuards, DeriveFunctor #-}
8{-# LANGUAGE PatternGuards, DeriveFunctor #-}
2
9
3module IRTS.Lang where
10module IRTS.Lang where
@@ -19,19 +26,19 @@ data LVar = Loc Int | Glob Name
19-- ASSUMPTION: All variable bindings have unique names here
26-- ASSUMPTION: All variable bindings have unique names here
20-- Constructors commented as lifted are not present in the LIR provided to the different backends.
27-- Constructors commented as lifted are not present in the LIR provided to the different backends.
21data LExp = LV LVar
28data LExp = LV LVar
22− | LApp Bool LExp [LExp] -- True = tail call
29+ | LApp Bool LExp [LExp] -- True = tail call
23− | LLazyApp Name [LExp] -- True = tail call
30+ | LLazyApp Name [LExp] -- True = tail call
24− | LLazyExp LExp -- lifted out before compiling
31+ | LLazyExp LExp -- lifted out before compiling
25− | LForce LExp -- make sure Exp is evaluted
32+ | LForce LExp -- make sure Exp is evaluted
26− | LLet Name LExp LExp -- name just for pretty printing
33+ | LLet Name LExp LExp -- name just for pretty printing
27− | LLam [Name] LExp -- lambda, lifted out before compiling
34+ | LLam [Name] LExp -- lambda, lifted out before compiling
28− | LProj LExp Int -- projection
35+ | LProj LExp Int -- projection
29− | LCon (Maybe LVar) -- Location to reallocate, if available
36+ | LCon (Maybe LVar) -- Location to reallocate, if available
30 Int Name [LExp]
37 Int Name [LExp]
31 | LCase CaseType LExp [LAlt]
38 | LCase CaseType LExp [LAlt]
32 | LConst Const
39 | LConst Const
33− | LForeign FDesc -- Function descriptor (usually name as string)
40+ | LForeign FDesc -- Function descriptor (usually name as string)
34− FDesc -- Return type descriptor
41+ FDesc -- Return type descriptor
35 [(FDesc, LExp)] -- first LExp is the FFI type description
42 [(FDesc, LExp)] -- first LExp is the FFI type description
36 | LOp PrimFn [LExp]
43 | LOp PrimFn [LExp]
37 | LNothing
44 | 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+-}
1{-# LANGUAGE PatternGuards, DeriveFunctor #-}
8{-# LANGUAGE PatternGuards, DeriveFunctor #-}
2
9
3module IRTS.LangOpts where
10module IRTS.LangOpts where
@@ -20,17 +27,19 @@ nextN = do i <- get
20 put (i + 1)
27 put (i + 1)
21 return $ sMN i "in"
28 return $ sMN i "in"
22
29
30+-- | Inline inside a declaration.
31+--
23−-- Inline inside a declaration. Variables are still Name at this stage.
32+-- Variables are still Name at this stage. Need to preserve
24−-- Need to preserve uniqueness of variable names in the resulting definition,
33+-- uniqueness of variable names in the resulting definition, so invent
25−-- so invent a new name for every variable we encounter
34+-- a new name for every variable we encounter
26doInline :: LDefs -> LDecl -> LDecl
35doInline :: LDefs -> LDecl -> LDecl
27doInline defs d@(LConstructor _ _ _) = d
36doInline defs d@(LConstructor _ _ _) = d
28−doInline defs (LFun opts topn args exp)
37+doInline defs (LFun opts topn args exp)
29 = let res = evalState (inlineWith [topn] (map (\n -> (n, LV (Glob n))) args) exp) 0 in
38 = let res = evalState (inlineWith [topn] (map (\n -> (n, LV (Glob n))) args) exp) 0 in
30 LFun opts topn args res
39 LFun opts topn args res
31 where
40 where
32 inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp
41 inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp
33− inlineWith done env var@(LV (Glob n))
42+ inlineWith done env var@(LV (Glob n))
34 = case lookup n env of
43 = case lookup n env of
35 Just t -> return t
44 Just t -> return t
36 Nothing -> return var
45 Nothing -> return var
@@ -39,7 +48,7 @@ doInline defs (LFun opts topn args exp)
39 inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e
48 inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e
40 -- Extend the environment for Let and Lam so that bound names aren't
49 -- Extend the environment for Let and Lam so that bound names aren't
41 -- expanded with any top level argument definitions they shadow
50 -- 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)
43 = do n' <- nextN
52 = do n' <- nextN
44 LLet n' <$> inlineWith done env val <*>
53 LLet n' <$> inlineWith done env val <*>
45 inlineWith done ((n, LV (Glob n')) : env) sc
54 inlineWith done ((n, LV (Glob n')) : env) sc
@@ -51,7 +60,7 @@ doInline defs (LFun opts topn args exp)
51 inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i
60 inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i
52 inlineWith done env (LCon loc i n es)
61 inlineWith done env (LCon loc i n es)
53 = LCon loc i n <$> mapM (inlineWith done env) es
62 = 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)
55 = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts
64 = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts
56 inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es
65 inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es
57 -- the interesting case!
66 -- the interesting case!
@@ -72,8 +81,7 @@ doInline defs (LFun opts topn args exp)
72 inlineWithAlt done env (LConCase i n es rhs)
81 inlineWithAlt done env (LConCase i n es rhs)
73 = do ns' <- mapM (\n -> do n' <- nextN
82 = do ns' <- mapM (\n -> do n' <- nextN
74 return (n, n')) es
83 return (n, n')) es
75− LConCase i n (map snd ns') <$>
84+ LConCase i n (map snd ns') <$>
76 inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs
85 inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs
77 inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e
86 inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e
78 inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e
87 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+-}
1{-# LANGUAGE OverloadedStrings #-}
8{-# LANGUAGE OverloadedStrings #-}
2−
3module IRTS.Portable (writePortable) where
9module IRTS.Portable (writePortable) where
4
10
5import Data.Aeson
11import 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+-}
1module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
8module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
2
9
3import IRTS.Defunctionalise
10import IRTS.Defunctionalise
@@ -9,9 +16,6 @@ import Control.Monad.State
9
16
10import Debug.Trace
17import Debug.Trace
11
18
12−-- Simplified expressions, where functions/constructors can only be applied
13−-- to variables
14−
15data SExp = SV LVar
19data SExp = SV LVar
16 | SApp Bool Name [LVar]
20 | SApp Bool Name [LVar]
17 | SLet LVar SExp SExp
21 | SLet LVar SExp SExp
@@ -231,4 +235,3 @@ scopecheck fn ctxt envTop tm = sc envTop tm where
231 return (SConstCase c e')
235 return (SConstCase c e')
232 scalt env (SDefaultCase e) = do e' <- sc env e
236 scalt env (SDefaultCase e) = do e' <- sc env e
233 return (SDefaultCase e')
237 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+-}
1{-# LANGUAGE CPP #-}
8{-# LANGUAGE CPP #-}
2−module IRTS.System(getDataFileName, getDataDir, getTargetDir,getCC,getLibFlags,getIdrisLibDir,
9+module IRTS.System( getDataFileName
10+ , getDataDir
11+ , getTargetDir
12+ , getCC
13+ , getLibFlags
14+ , getIdrisLibDir
3− getIncFlags, getEnvFlags, version) where
15+ , getIncFlags
16+ , getEnvFlags
17+ , version
18+ ) where
4
19
5import Data.List.Split
20import Data.List.Split
6
21
src/Idris/ASTUtils.hs+45−35
@@ -1,38 +1,48 @@
1−module Idris.ASTUtils(Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState,
1+{-|
2− fputState, idris_fixities, ist_callgraph, ist_optimisation,
2+Module : Idris.ASTUtils
3− known_classes, known_terms, opt_detaggable, opt_inaccessible,
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− opts_idrisCmdline, repl_definitions) where
4+Copyright :
5−
5+License : BSD3
6+Maintainer : The Idris Community.
7+
6−-- This implements just a few basic lens-like concepts to ease state updates.
8+This implements just a few basic lens-like concepts to ease state updates.
7−-- Similar to fclabels in approach, just without the extra dependency.
9+Similar to fclabels in approach, just without the extra dependency.
8−--
10+
9−-- We don't include an explicit export list
11+We don't include an explicit export list
10−-- because everything here is meant to be exported.
12+because everything here is meant to be exported.
11−--
13+
12−-- Short synopsis:
14+Short synopsis:
13−-- ---------------
15+---------------
14−--
16+@
15−-- f :: Idris ()
17+f :: Idris ()
16−-- f = do
18+f = do
17−-- -- these two steps:
19+ -- these two steps:
18−-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
20+ detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
19−-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)
21+ fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)
20−--
22+
21−-- -- are equivalent to:
23+ -- are equivalent to:
22−-- fmodifyState (opt_detaggable . ist_optimisation typeName) not
24+ fmodifyState (opt_detaggable . ist_optimisation typeName) not
23−--
25+
24−-- -- of course, the long accessor can be put in a variable;
26+ -- of course, the long accessor can be put in a variable;
25−-- -- everything is first-class
27+ -- everything is first-class
26−-- let detag n = opt_detaggable . ist_optimisation n
28+ let detag n = opt_detaggable . ist_optimisation n
27−-- fputState (detag n1) True
29+ fputState (detag n1) True
28−-- fputState (detag n2) False
30+ fputState (detag n2) False
29−--
31+
30−-- -- Note that all these operations handle missing items consistently
32+ -- Note that all these operations handle missing items consistently
31−-- -- and transparently, as prescribed by the default values included
33+ -- and transparently, as prescribed by the default values included
32−-- -- in the definitions of the ist_* functions.
34+ -- in the definitions of the ist_* functions.
33−-- --
35+ --
34−-- -- Especially, it's no longer necessary to have initial values of
36+ -- Especially, it's no longer necessary to have initial values of
35−-- -- data structures copied (possibly inconsistently) all over the compiler.
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
36
46
37import Control.Category
47import Control.Category
38import Control.Applicative
48import 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+-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
9 TypeSynonymInstances, PatternGuards #-}
3
10
11+module Idris.AbsSyntax(
12+ module Idris.AbsSyntax
4−module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
13+ , module Idris.AbsSyntaxTree
14+ ) where
5
15
6import Idris.Core.TT
16import Idris.Core.TT
7import Idris.Core.Evaluate
17import 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+-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
9 DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
3
10
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+-}
1module Idris.Apropos (apropos, aproposModules) where
8module Idris.Apropos (apropos, aproposModules) where
2
9
3import Idris.AbsSyntax
10import 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+-}
1{-# LANGUAGE PatternGuards #-}
20{-# LANGUAGE PatternGuards #-}
2
21
22+module Idris.CaseSplit(
3−module Idris.CaseSplit(splitOnLine, replaceSplits,
23+ splitOnLine, replaceSplits
4− getClause, getProofClause,
24+ , getClause, getProofClause
5− mkWith,
25+ , mkWith
6− nameMissing,
26+ , nameMissing
7− getUniq, nameRoot) where
27+ , getUniq, nameRoot
8−-- splitting a variable in a pattern clause
28+ ) where
9
29
10import Idris.AbsSyntax
30import Idris.AbsSyntax
11import Idris.AbsSyntaxTree (Idris, IState, PTerm)
31import Idris.AbsSyntaxTree (Idris, IState, PTerm)
@@ -36,20 +56,6 @@ import Text.Trifecta.Delta
36
56
37import Debug.Trace
57import Debug.Trace
38
58
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−
53-- | Given a variable to split, and a term application, return a list
59-- | Given a variable to split, and a term application, return a list
54-- of variable updates, paired with a flag to say whether the given
60-- of variable updates, paired with a flag to say whether the given
55-- update typechecks (False = impossible) if the flag is 'False' the
61-- update typechecks (False = impossible) if the flag is 'False' the
@@ -289,7 +295,7 @@ replaceSplits l ups impossible
289 updateRHSs 1 (map (rep ist (expandBraces l)) ups)
295 updateRHSs 1 (map (rep ist (expandBraces l)) ups)
290 where
296 where
291 rep ist str [] = str ++ "\n"
297 rep ist str [] = str ++ "\n"
292− rep ist str ((n, tm) : ups)
298+ rep ist str ((n, tm) : ups)
293 = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups
299 = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups
294
300
295 updateRHSs i [] = return []
301 updateRHSs i [] = return []
src/Idris/Chaser.hs+12−1
@@ -1,4 +1,15 @@
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(
1−module Idris.Chaser(buildTree, getImports, getModuleFiles, ModuleTree(..)) where
9+ buildTree, getImports
10+ , getModuleFiles
11+ , ModuleTree(..)
12+ ) where
2
13
3import Idris.Core.TT
14import Idris.Core.TT
4import Idris.Parser
15import 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+-}
1{-# LANGUAGE Arrows #-}
8{-# LANGUAGE Arrows #-}
2module Idris.CmdOptions where
9module Idris.CmdOptions where
3
10
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+-}
1module Idris.Colours (
8module Idris.Colours (
2− IdrisColour(..),
9+ IdrisColour(..)
3− ColourTheme(..),
10+ , ColourTheme(..)
4− defaultTheme,
11+ , defaultTheme
5− colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,
12+ , colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate
6− colouriseType, colouriseFun, colouriseData, colouriseKeyword,
13+ , colouriseType, colouriseFun, colouriseData, colouriseKeyword
7− colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise) where
14+ , colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise
15+ ) where
8
16
9import System.Console.ANSI
17import System.Console.ANSI
10import System.IO (Handle)
18import System.IO (Handle)
src/Idris/Completion.hs+7−1
@@ -1,4 +1,10 @@
1+{-|
2+Module : Idris.Completion
1−-- | Support for command-line completion at the REPL and in the prover
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+-}
2module Idris.Completion (replCompletion, proverCompletion) where
8module Idris.Completion (replCompletion, proverCompletion) where
3
9
4import Idris.Core.Evaluate (ctxtAlist)
10import 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+-}
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2−
3−{-| Binary instances for the core datatypes -}
4module Idris.Core.Binary where
9module Idris.Core.Binary where
5
10
6import Control.Applicative ((<*>), (<$>))
11import Control.Applicative ((<*>), (<$>))
@@ -271,7 +276,7 @@ instance Binary a => Binary (Err' a) where
271
276
272instance Binary FC where
277instance Binary FC where
273 put x =
278 put x =
274− case x of
279+ case x of
275 (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0
280 (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0
276 put x1
281 put x1
277 put (x2 * 65536 + x3)
282 put (x2 * 65536 + x3)
@@ -589,7 +594,7 @@ instance Binary UExp where
589 put x = case x of
594 put x = case x of
590 UVar t -> do putWord8 0
595 UVar t -> do putWord8 0
591 put ((-1) :: Int) -- TMP HACK!
596 put ((-1) :: Int) -- TMP HACK!
592− UVal t -> do putWord8 1
597+ UVal t -> do putWord8 1
593 put t
598 put t
594
599
595 get = do i <- getWord8
600 get = do i <- getWord8
@@ -653,7 +658,7 @@ instance {- (Binary n) => -} Binary (TT Name) where
653 x2 <- getWord8
658 x2 <- getWord8
654 return (Proj x1 ((fromEnum x2)-1))
659 return (Proj x1 ((fromEnum x2)-1))
655 6 -> return Erased
660 6 -> return Erased
656− 7 -> do x1 <- get
661+ 7 -> do x1 <- get
657 return (TType x1)
662 return (TType x1)
658 8 -> return Impossible
663 8 -> return Impossible
659 9 -> do x1 <- get
664 9 -> do x1 <- get
@@ -661,4 +666,3 @@ instance {- (Binary n) => -} Binary (TT Name) where
661 10 -> do x1 <- get
666 10 -> do x1 <- get
662 return (UType x1)
667 return (UType x1)
663 _ -> error "Corrupted binary data for TT"
668 _ -> 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+-}
1{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
21{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
2
22
23+module Idris.Core.CaseTree (
3−module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo,
24+ CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
4− Phase(..), CaseTree, CaseType(..),
25+ , Phase(..), CaseTree, CaseType(..)
5− simpleCase, small, namesUsed, findCalls, findUsedArgs,
26+ , simpleCase, small, namesUsed, findCalls, findUsedArgs
6− substSC, substAlt, mkForce) where
27+ , substSC, substAlt, mkForce
28+ ) where
7
29
8import Idris.Core.TT
30import Idris.Core.TT
9
31
@@ -18,18 +40,6 @@ import Debug.Trace
18data CaseDef = CaseDef [Name] !SC [Term]
40data CaseDef = CaseDef [Name] !SC [Term]
19 deriving Show
41 deriving Show
20
42
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−--
33data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first
43data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first
34 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
44 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
35 | STerm !t
45 | STerm !t
src/Idris/Core/Constraints.hs+8−2
@@ -1,7 +1,13 @@
1+{-|
2+Module : Idris.Core.Constraints
1−-- | Check universe constraints.
3+Description : Check universe constraints.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
2module Idris.Core.Constraints ( ucheck ) where
8module Idris.Core.Constraints ( ucheck ) where
3
9
4−import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),
10+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),
5 ConstraintFC(..), Err'(..) )
11 ConstraintFC(..), Err'(..) )
6
12
7import Control.Applicative
13import 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+-}
1{-# LANGUAGE BangPatterns, ViewPatterns #-}
8{-# LANGUAGE BangPatterns, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3
10
@@ -241,14 +248,14 @@ instance NFData Accessibility where
241 rnf Hidden = ()
248 rnf Hidden = ()
242 rnf Private = ()
249 rnf Private = ()
243
250
244−
251+
245instance NFData Totality where
252instance NFData Totality where
246 rnf (Total x1) = rnf x1 `seq` ()
253 rnf (Total x1) = rnf x1 `seq` ()
247 rnf Productive = ()
254 rnf Productive = ()
248 rnf (Partial x1) = rnf x1 `seq` ()
255 rnf (Partial x1) = rnf x1 `seq` ()
249 rnf Unchecked = ()
256 rnf Unchecked = ()
250 rnf Generated = ()
257 rnf Generated = ()
251−
258+
252instance NFData PReason where
259instance NFData PReason where
253 rnf (Other x1) = rnf x1 `seq` ()
260 rnf (Other x1) = rnf x1 `seq` ()
254 rnf Itself = ()
261 rnf Itself = ()
@@ -274,7 +281,7 @@ instance NFData Def where
274
281
275instance NFData CaseInfo where
282instance NFData CaseInfo where
276 rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
283 rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
277−
284+
278instance NFData CaseDefs where
285instance NFData CaseDefs where
279 rnf (CaseDefs x1 x2 x3 x4)
286 rnf (CaseDefs x1 x2 x3 x4)
280 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
287 = 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 #-}
1+{-|
2−
2+Module : Idris.Core.Elaborate
3−{- A high level language of tactic composition, for building
4− elaborators from a high level language into the core theory.
3+Description : A high level language of tactic composition, for building elaborators from a high level language into the core theory.
5−
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+
6− This is our interface to proof construction, rather than
8+This is our interface to proof construction, rather than ProofState,
7− ProofState, because this gives us a language to build derived
9+because this gives us a language to build derived tactics out of the
8− tactics out of the primitives.
10+primitives.
9-}
11-}
10
12
13+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
11−module Idris.Core.Elaborate(module Idris.Core.Elaborate,
14+module Idris.Core.Elaborate (
15+ module Idris.Core.Elaborate
12− module Idris.Core.ProofState) where
16+ , module Idris.Core.ProofState
17+ ) where
13
18
14import Idris.Core.ProofState
19import Idris.Core.ProofState
15import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,
20import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,
@@ -51,7 +56,7 @@ explicit n = do ES (p, a) s m <- get
51 let p' = p { dontunify = n : dontunify p }
56 let p' = p { dontunify = n : dontunify p }
52 put (ES (p', a) s m)
57 put (ES (p', a) s m)
53
58
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
55-- it was given explicitly on the lhs, or intrduced as an explicit lambda
60-- it was given explicitly on the lhs, or intrduced as an explicit lambda
56-- or let binding)
61-- or let binding)
57addPSname :: Name -> Elab' aux ()
62addPSname :: Name -> Elab' aux ()
@@ -78,11 +83,11 @@ loadState = do (ES p s e) <- get
78getNameFrom :: Name -> Elab' aux Name
83getNameFrom :: Name -> Elab' aux Name
79getNameFrom n = do (ES (p, a) s e) <- get
84getNameFrom n = do (ES (p, a) s e) <- get
80 let next = nextname p
85 let next = nextname p
81− let p' = p { nextname = next + 1 }
86+ let p' = p { nextname = next + 1 }
82 put (ES (p', a) s e)
87 put (ES (p', a) s e)
83 let n' = case n of
88 let n' = case n of
84 UN x -> MN (next+100) x
89 UN x -> MN (next+100) x
85− MN i x -> if i == 99999
90+ MN i x -> if i == 99999
86 then MN (next+500) x
91 then MN (next+500) x
87 else MN (next+100) x
92 else MN (next+100) x
88 NS (UN x) s -> MN (next+100) x
93 NS (UN x) s -> MN (next+100) x
@@ -97,7 +102,7 @@ setNextName = do env <- get_env
97
102
98initNextNameFrom :: [Name] -> Elab' aux ()
103initNextNameFrom :: [Name] -> Elab' aux ()
99initNextNameFrom ns = do ES (p, a) s e <- get
104initNextNameFrom ns = do ES (p, a) s e <- get
100− let n' = maxName (nextname p) ns
105+ let n' = maxName (nextname p) ns
101 put (ES (p { nextname = n' }, a) s e)
106 put (ES (p { nextname = n' }, a) s e)
102 where
107 where
103 maxName m ((MN i _) : xs) = maxName (max m i) xs
108 maxName m ((MN i _) : xs) = maxName (max m i) xs
@@ -124,7 +129,7 @@ errAt thing n ty = transformErr (Elaborating thing n ty)
124
129
125
130
126erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)
131erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)
127−erunAux f elab
132+erunAux f elab
128 = do s <- get
133 = do s <- get
129 case runStateT elab s of
134 case runStateT elab s of
130 OK (a, s') -> do put s'
135 OK (a, s') -> do put s'
@@ -489,16 +494,16 @@ dotterm = do ES (p, a) s m <- get
489 tm <- get_term
494 tm <- get_term
490 case holes p of
495 case holes p of
491 [] -> return ()
496 [] -> return ()
492− (h : hs) ->
497+ (h : hs) ->
493 do let outer = findOuter h [] tm
498 do let outer = findOuter h [] tm
494 let p' = p { dotted = (h, outer) : dotted p }
499 let p' = p { dotted = (h, outer) : dotted p }
495−-- trace ("DOTTING " ++ show (h, outer) ++ "\n" ++
500+-- trace ("DOTTING " ++ show (h, outer) ++ "\n" ++
496-- show tm) $
501-- show tm) $
497 put $ ES (p', a) s m
502 put $ ES (p', a) s m
498 where
503 where
499 findOuter h env (P _ n _) | h == n = env
504 findOuter h env (P _ n _) | h == n = env
500 findOuter h env (Bind n b sc)
505 findOuter h env (Bind n b sc)
501− = union (foB b)
506+ = union (foB b)
502 (findOuter h env (instantiate (P Bound n (binderTy b)) sc))
507 (findOuter h env (instantiate (P Bound n (binderTy b)) sc))
503 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)
508 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)
504 foB (Let t v) = union (findOuter h env t) (findOuter h env v)
509 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
506 findOuter h env (App _ f a)
511 findOuter h env (App _ f a)
507 = union (findOuter h env f) (findOuter h env a)
512 = union (findOuter h env f) (findOuter h env a)
508 findOuter h env _ = []
513 findOuter h env _ = []
509−
514+
510
515
511get_dotterm :: Elab' aux [(Name, [Name])]
516get_dotterm :: Elab' aux [(Name, [Name])]
512get_dotterm = do ES (p, a) s m <- get
517get_dotterm = do ES (p, a) s m <- get
@@ -566,8 +571,8 @@ prepare_apply fn imps =
566 env <- get_env
571 env <- get_env
567 -- let claims = getArgs ty imps
572 -- let claims = getArgs ty imps
568 -- claims <- mkClaims (normalise ctxt env ty) imps []
573 -- claims <- mkClaims (normalise ctxt env ty) imps []
569− claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
574+ claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
570− mkClaims (finalise ty)
575+ mkClaims (finalise ty)
571 (normalise ctxt env (finalise ty))
576 (normalise ctxt env (finalise ty))
572 imps [] (map fst env)
577 imps [] (map fst env)
573 ES (p, a) s prev <- get
578 ES (p, a) s prev <- get
@@ -583,7 +588,7 @@ prepare_apply fn imps =
583 -> [(Name, Name)] -- ^ Accumulator for produced claims
588 -> [(Name, Name)] -- ^ Accumulator for produced claims
584 -> [Name] -- ^ Hypotheses
589 -> [Name] -- ^ Hypotheses
585 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.
590 -> 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 =
587 do let t = rebind hs t_in
592 do let t = rebind hs t_in
588 n <- getNameFrom (mkMN n')
593 n <- getNameFrom (mkMN n')
589-- when (null claims) (start_unify n)
594-- when (null claims) (start_unify n)
@@ -657,7 +662,7 @@ apply' fillt fn imps =
657
662
658 getNonUnify acc [] _ = acc
663 getNonUnify acc [] _ = acc
659 getNonUnify acc _ [] = acc
664 getNonUnify acc _ [] = acc
660− getNonUnify acc ((i,_):is) ((a, t):as)
665+ getNonUnify acc ((i,_):is) ((a, t):as)
661 | i = getNonUnify acc is as
666 | i = getNonUnify acc is as
662 | otherwise = getNonUnify (t : acc) is as
667 | otherwise = getNonUnify (t : acc) is as
663
668
@@ -787,7 +792,7 @@ infer_app infer fun arg str =
787 end_unify
792 end_unify
788
793
789dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
794dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
790−dep_app fun arg str =
795+dep_app fun arg str =
791 do a <- getNameFrom (sMN 0 "__argTy")
796 do a <- getNameFrom (sMN 0 "__argTy")
792 b <- getNameFrom (sMN 0 "__retTy")
797 b <- getNameFrom (sMN 0 "__retTy")
793 fty <- getNameFrom (sMN 0 "__fnTy")
798 fty <- getNameFrom (sMN 0 "__fnTy")
@@ -800,13 +805,13 @@ dep_app fun arg str =
800 g <- goal
805 g <- goal
801 start_unify s
806 start_unify s
802 claim s (Var a)
807 claim s (Var a)
803−
808+
804 prep_fill f [s]
809 prep_fill f [s]
805 focus f; attack; fun
810 focus f; attack; fun
806 end_unify
811 end_unify
807 fty <- goal
812 fty <- goal
808 solve
813 solve
809− focus s; attack;
814+ focus s; attack;
810 ctxt <- get_context
815 ctxt <- get_context
811 env <- get_env
816 env <- get_env
812 case normalise ctxt env fty of
817 case normalise ctxt env fty of
@@ -856,7 +861,7 @@ no_errors tac err
856 ((x, y, _, env, inerr, while, _) : _) ->
861 ((x, y, _, env, inerr, while, _) : _) ->
857 let (xp, yp) = getProvenance inerr
862 let (xp, yp) = getProvenance inerr
858 env' = map (\(x, b) -> (x, binderTy b)) env in
863 env' = map (\(x, b) -> (x, binderTy b)) env in
859− lift $ tfail $
864+ lift $ tfail $
860 case err of
865 case err of
861 Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0
866 Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0
862 Just e -> e
867 Just e -> e
@@ -867,7 +872,7 @@ try :: Elab' aux a -> Elab' aux a -> Elab' aux a
867try t1 t2 = try' t1 t2 False
872try t1 t2 = try' t1 t2 False
868
873
869handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
874handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
870−handleError p t1 t2
875+handleError p t1 t2
871 = do s <- get
876 = do s <- get
872 ps <- get_probs
877 ps <- get_probs
873 case runStateT t1 s of
878 case runStateT t1 s of
@@ -907,7 +912,7 @@ try' t1 t2 proofSearch
907 recoverableErr _ = True
912 recoverableErr _ = True
908
913
909tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
914tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
910−tryCatch t1 t2
915+tryCatch t1 t2
911 = do s <- get
916 = do s <- get
912 ps <- get_probs
917 ps <- get_probs
913 ulog <- getUnifyLog
918 ulog <- getUnifyLog
@@ -953,7 +958,7 @@ tryAll' constrok xs = doAll [] 999999 xs
953 ivs <- get_instances
958 ivs <- get_instances
954 case prunStateT pmax True ps (if constrok then Nothing
959 case prunStateT pmax True ps (if constrok then Nothing
955 else Just ivs) x s of
960 else Just ivs) x s of
956− OK ((v, newps, probs), s') ->
961+ OK ((v, newps, probs), s') ->
957 do let cs' = if (newps < pmax)
962 do let cs' = if (newps < pmax)
958 then [do put s'; return $! v]
963 then [do put s'; return $! v]
959 else (do put s'; return $! v) : cs
964 else (do put s'; return $! v) : cs
@@ -980,7 +985,7 @@ prunStateT pmax zok ps ivs x s
980 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
985 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
981 then case reverse (problems p) of
986 then case reverse (problems p) of
982 ((_,_,_,_,e,_,_):_) -> Error e
987 ((_,_,_,_,e,_,_):_) -> Error e
983− else if ibad
988+ else if ibad
984 then Error (InternalMsg "Constraint introduced in disambiguation")
989 then Error (InternalMsg "Constraint introduced in disambiguation")
985 else OK ((v, newpmax, problems p), s')
990 else OK ((v, newpmax, problems p), s')
986 Error e -> Error e
991 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+-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,
2 PatternGuards #-}
9 PatternGuards #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4
11
5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
12+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
6 normaliseAll, normaliseBlocking, toValue, quoteTerm,
13 normaliseAll, normaliseBlocking, toValue, quoteTerm,
7 rt_simplify, simplify, specialise, hnf, convEq, convEq',
14 rt_simplify, simplify, specialise, hnf, convEq, convEq',
8 Def(..), CaseInfo(..), CaseDefs(..),
15 Def(..), CaseInfo(..), CaseDefs(..),
@@ -12,7 +19,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
12 addDatatype, addCasedef, simplifyCasedef, addOperator,
19 addDatatype, addCasedef, simplifyCasedef, addOperator,
13 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
20 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
14 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
21 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
15− mapDefCtxt,
22+ mapDefCtxt,
16 lookupTotal, lookupTotalExact, lookupInjectiveExact,
23 lookupTotal, lookupTotalExact, lookupInjectiveExact,
17 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
24 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
18 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
25 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
@@ -103,7 +110,7 @@ normaliseTrace tr ctxt env t
103 quote 0 val) initEval
110 quote 0 val) initEval
104
111
105toValue :: Context -> Env -> TT Name -> Value
112toValue :: Context -> Env -> TT Name -> Value
106−toValue ctxt env t
113+toValue ctxt env t
107 = evalState (eval False ctxt [] (map finalEntry env) t []) initEval
114 = evalState (eval False ctxt [] (map finalEntry env) t []) initEval
108
115
109quoteTerm :: Value -> TT Name
116quoteTerm :: Value -> TT Name
@@ -596,9 +603,9 @@ convEq ctxt holes topx topy = ceq [] topx topy where
596 | x `elem` holes || y `elem` holes = return True
603 | x `elem` holes || y `elem` holes = return True
597 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
604 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
598 | otherwise = sameDefs ps x y
605 | 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)))
600 = ceq ps x (substV (P Bound n t) y)
607 = 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
602 = ceq ps (substV (P Bound n t) x) y
609 = ceq ps (substV (P Bound n t) x) y
603 ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))
610 ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))
604 | n == n' = ceq ps x y
611 | n == n' = ceq ps x y
@@ -746,9 +753,9 @@ instance Show Def where
746-- Hidden => Programs can't access the name at all
753-- Hidden => Programs can't access the name at all
747-- Public => Programs can access the name and use at will
754-- Public => Programs can access the name and use at will
748-- Frozen => Programs can access the name, which doesn't reduce
755-- 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
750
757
751−data Accessibility = Hidden | Public | Frozen | Private
758+data Accessibility = Hidden | Public | Frozen | Private
752 deriving (Eq, Ord)
759 deriving (Eq, Ord)
753{-!
760{-!
754deriving instance NFData Accessibility
761deriving instance NFData Accessibility
@@ -993,7 +1000,7 @@ lookupTyName n ctxt = do
993
1000
994-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
1001-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
995lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
1002lookupTyNameExact :: 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 ]
997
1004
998-- | Get the types that match some name
1005-- | Get the types that match some name
999lookupTy :: Name -> Context -> [Type]
1006lookupTy :: Name -> Context -> [Type]
@@ -1048,7 +1055,7 @@ lookupP = lookupP_all False False
1048
1055
1049lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
1056lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
1050lookupP_all all exact n ctxt
1057lookupP_all all exact n ctxt
1051− = do (n', def) <- names
1058+ = do (n', def) <- names
1052 p <- case def of
1059 p <- case def of
1053 (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)
1060 (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)
1054 (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)
1061 (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)
@@ -1060,7 +1067,7 @@ lookupP_all all exact n ctxt
1060 _ -> return (fst p)
1067 _ -> return (fst p)
1061 where
1068 where
1062 names = let ns = lookupCtxtName n (definitions ctxt) in
1069 names = let ns = lookupCtxtName n (definitions ctxt) in
1063− if exact
1070+ if exact
1064 then filter (\ (n', d) -> n' == n) ns
1071 then filter (\ (n', d) -> n' == n) ns
1065 else ns
1072 else ns
1066
1073
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+
1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
9{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Core.Execute (execute) where
11module Idris.Core.Execute (execute) where
@@ -112,7 +120,7 @@ toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
112 return $ normalise ctxt env' tm
120 return $ normalise ctxt env' tm
113 where toBinder (n, v) = do v' <- toTT v
121 where toBinder (n, v) = do v' <- toTT v
114 return (n, Let Erased v')
122 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."
116toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."
124toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."
117
125
118unApplyV :: ExecVal -> (ExecVal, [ExecVal])
126unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -251,7 +259,7 @@ execApp env ctxt c@(EP (TCon _ arity) n _) args =
251 let restArgs = drop arity args
259 let restArgs = drop arity args
252 execApp env ctxt (mkEApp c args') restArgs
260 execApp env ctxt (mkEApp c args') restArgs
253
261
254−execApp env ctxt f@(EP _ n _) args
262+execApp env ctxt f@(EP _ n _) args
255 | Just (res, rest) <- getOp n args = do r <- res
263 | Just (res, rest) <- getOp n args = do r <- res
256 execApp env ctxt r rest
264 execApp env ctxt r rest
257execApp env ctxt f@(EP _ n _) args =
265execApp env ctxt f@(EP _ n _) args =
@@ -388,7 +396,7 @@ execForeign env ctxt arity ty fn xs onfail
388
396
389-- Right now, there's no way to send command-line arguments to the executor,
397-- Right now, there's no way to send command-line arguments to the executor,
390-- so just return 0.
398-- so just return 0.
391−execForeign env ctxt arity ty fn xs onfail
399+execForeign env ctxt arity ty fn xs onfail
392 | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
400 | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
393 = let res = ioWrap . EConstant . I $ 0
401 = let res = ioWrap . EConstant . I $ 0
394 in execApp env ctxt res (drop arity xs)
402 in execApp env ctxt res (drop arity xs)
@@ -410,8 +418,8 @@ splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
410 = Just (toFDesc l, r)
418 = Just (toFDesc l, r)
411splitArg _ = Nothing
419splitArg _ = Nothing
412
420
413−toFDesc tm
421+toFDesc tm
414− | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
422+ | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
415 | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
423 | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
416toFDesc _ = FUnknown
424toFDesc _ = FUnknown
417
425
@@ -432,7 +440,7 @@ upio = sUN "unsafePerformPrimIO"
432delay = sUN "Delay"
440delay = sUN "Delay"
433force = sUN "Force"
441force = sUN "Force"
434
442
435−-- | Look up primitive operations in the global table and transform
443+-- | Look up primitive operations in the global table and transform
436-- them into ExecVal functions
444-- them into ExecVal functions
437getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
445getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
438getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)
446getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)
@@ -463,14 +471,14 @@ getOp fn (_ : EHandle h : xs)
463getOp fn (_ : arg : xs)
471getOp fn (_ : arg : xs)
464 | fn == prf =
472 | fn == prf =
465 Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)
473 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
474+getOp n args = do (arity, prim) <- getPrim n primitives
467− if (length args >= arity)
475+ if (length args >= arity)
468 then do res <- applyPrim prim (take arity args)
476 then do res <- applyPrim prim (take arity args)
469 Just (res, drop arity args)
477 Just (res, drop arity args)
470 else Nothing
478 else Nothing
471 where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
479 where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
472 getPrim n [] = Nothing
480 getPrim n [] = Nothing
473− getPrim n ((Prim pn _ arity def _ _) : prims)
481+ getPrim n ((Prim pn _ arity def _ _) : prims)
474 | n == pn = Just (arity, execPrim def)
482 | n == pn = Just (arity, execPrim def)
475 | otherwise = getPrim n prims
483 | otherwise = getPrim n prims
476
484
@@ -534,15 +542,15 @@ chooseAlt _ [] = Nothing
534data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
542data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
535
543
536toFType :: FDesc -> FType
544toFType :: FDesc -> FType
537−toFType (FCon c)
545+toFType (FCon c)
538 | c == sUN "C_Str" = FString
546 | c == sUN "C_Str" = FString
539 | c == sUN "C_Float" = FArith ATFloat
547 | c == sUN "C_Float" = FArith ATFloat
540 | c == sUN "C_Ptr" = FPtr
548 | c == sUN "C_Ptr" = FPtr
541 | c == sUN "C_MPtr" = FManagedPtr
549 | c == sUN "C_MPtr" = FManagedPtr
542 | c == sUN "C_Unit" = FUnit
550 | c == sUN "C_Unit" = FUnit
543−toFType (FApp c [_,ity])
551+toFType (FApp c [_,ity])
544 | c == sUN "C_IntT" = FArith (toAType ity)
552 | c == sUN "C_IntT" = FArith (toAType ity)
545− where toAType (FCon i)
553+ where toAType (FCon i)
546 | i == sUN "C_IntChar" = ATInt ITChar
554 | i == sUN "C_IntChar" = ATInt ITChar
547 | i == sUN "C_IntNative" = ATInt ITNative
555 | i == sUN "C_IntNative" = ATInt ITNative
548 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
556 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
@@ -551,14 +559,14 @@ toFType (FApp c [_,ity])
551 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
559 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
552 toAType t = error (show t ++ " not defined in toAType")
560 toAType t = error (show t ++ " not defined in toAType")
553
561
554−toFType (FApp c [_])
562+toFType (FApp c [_])
555 | c == sUN "C_Any" = FAny
563 | c == sUN "C_Any" = FAny
556toFType t = error (show t ++ " not defined in toFType")
564toFType t = error (show t ++ " not defined in toFType")
557
565
558call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
566call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
559call (FFun name argTypes retType) args =
567call (FFun name argTypes retType) args =
560 do fn <- findForeign name
568 do fn <- findForeign name
561− maybe (return Nothing)
569+ maybe (return Nothing)
562 (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
570 (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
563 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
571 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
564 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
572 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
src/Idris/Core/ProofState.hs+37−28
@@ -1,12 +1,22 @@
1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
1+{-|
2−
2+Module : Idris.Core.ProofState
3+Description : Proof state implementation.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+
3−{- Implements a proof state, some primitive tactics for manipulating
8+Implements a proof state, some primitive tactics for manipulating
4− proofs, and some high level commands for introducing new theorems,
9+proofs, and some high level commands for introducing new theorems,
5− evaluation/checking inside the proof system, etc. --}
10+evaluation/checking inside the proof system, etc.
11+-}
6
12
13+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
14+module Idris.Core.ProofState(
7−module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
15+ ProofState(..), newProof, envAtFocus, goalAtFocus
8− Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,
16+ , Tactic(..), Goal(..), processTactic, nowElaboratingPS
17+ , doneElaboratingAppPS, doneElaboratingArgPS, dropGiven
9− doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where
18+ , keepGiven, getProvenance
19+ ) where
10
20
11import Idris.Core.Typecheck
21import Idris.Core.Typecheck
12import Idris.Core.Evaluate
22import Idris.Core.Evaluate
@@ -134,7 +144,7 @@ instance Pretty ProofState OutputAnnotation where
134 pretty (thname ps) <+> colon <+> text " no more goals."
144 pretty (thname ps) <+> colon <+> text " no more goals."
135 pretty ps | (h : hs) <- holes ps =
145 pretty ps | (h : hs) <- holes ps =
136 let tm = pterm ps
146 let tm = pterm ps
137− OK g = goal (Just h) tm
147+ OK g = goal (Just h) tm
138 nm = thname ps in
148 nm = thname ps in
139 let wkEnv = premises g in
149 let wkEnv = premises g in
140 text "Other goals" <+> colon <+> pretty hs <+>
150 text "Other goals" <+> colon <+> pretty hs <+>
@@ -160,8 +170,8 @@ holeName i = sMN i "hole"
160qshow :: Fails -> String
170qshow :: Fails -> String
161qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fst env, x, y, hs)) fs)
171qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fst env, x, y, hs)) fs)
162
172
163−match_unify' :: Context -> Env ->
173+match_unify' :: Context -> Env ->
164− (TT Name, Maybe Provenance) ->
174+ (TT Name, Maybe Provenance) ->
165 (TT Name, Maybe Provenance) ->
175 (TT Name, Maybe Provenance) ->
166 StateT TState TC [(Name, TT Name)]
176 StateT TState TC [(Name, TT Name)]
167match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
177match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
@@ -184,7 +194,7 @@ match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
184 return u
194 return u
185 Error e -> traceWhen (unifylog ps)
195 Error e -> traceWhen (unifylog ps)
186 ("No match " ++ show e) $
196 ("No match " ++ show e) $
187− do put (ps { problems = (topx, topy, True,
197+ do put (ps { problems = (topx, topy, True,
188 env, e, while, Match) :
198 env, e, while, Match) :
189 problems ps })
199 problems ps })
190 return []
200 return []
@@ -217,8 +227,8 @@ dropSwaps (p@(x, P _ y _) : xs) | solvedIn y x xs = dropSwaps xs
217 solvedIn y x (_ : xs) = solvedIn y x xs
227 solvedIn y x (_ : xs) = solvedIn y x xs
218dropSwaps (p : xs) = p : dropSwaps xs
228dropSwaps (p : xs) = p : dropSwaps xs
219
229
220−unify' :: Context -> Env ->
230+unify' :: Context -> Env ->
221− (TT Name, Maybe Provenance) ->
231+ (TT Name, Maybe Provenance) ->
222 (TT Name, Maybe Provenance) ->
232 (TT Name, Maybe Provenance) ->
223 StateT TState TC [(Name, TT Name)]
233 StateT TState TC [(Name, TT Name)]
224unify' ctxt env (topx, xfrom) (topy, yfrom) =
234unify' ctxt env (topx, xfrom) (topy, yfrom) =
@@ -539,7 +549,7 @@ match_fill guess ctxt env (Bind x (Hole ty) sc) =
539 do (val, valty) <- lift $ check ctxt env guess
549 do (val, valty) <- lift $ check ctxt env guess
540-- let valtyn = normalise ctxt env valty
550-- let valtyn = normalise ctxt env valty
541-- let tyn = normalise ctxt env ty
551-- 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)
543 (ty, Just ExpectedType)
553 (ty, Just ExpectedType)
544 ps <- get
554 ps <- get
545 let (uh, uns) = unified ps
555 let (uh, uns) = unified ps
@@ -558,7 +568,7 @@ complete_fill :: RunTactic
558complete_fill ctxt env (Bind x (Guess ty val) sc) =
568complete_fill ctxt env (Bind x (Guess ty val) sc) =
559 do let guess = forget val
569 do let guess = forget val
560 (val', valty) <- lift $ check ctxt env guess
570 (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')
562 (ty, Just ExpectedType)
572 (ty, Just ExpectedType)
563 ps <- get
573 ps <- get
564 let (uh, uns) = unified ps
574 let (uh, uns) = unified ps
@@ -577,7 +587,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
577 dropdots <-
587 dropdots <-
578 case lookup x (notunified ps) of
588 case lookup x (notunified ps) of
579 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
589 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)
581 (val, Just GivenVal)
591 (val, Just GivenVal)
582 return [x]
592 return [x]
583 _ -> return []
593 _ -> return []
@@ -608,12 +618,12 @@ solve ctxt env (Bind x (Guess ty val) sc)
608 tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)
618 tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)
609 tryLock hs t@(Bind n (Hole _) sc) = (t, False)
619 tryLock hs t@(Bind n (Hole _) sc) = (t, False)
610 tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)
620 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)
612 = let (ty', tyl) = tryLock hs ty
622 = let (ty', tyl) = tryLock hs ty
613 (val', vall) = tryLock hs val
623 (val', vall) = tryLock hs val
614 (sc', scl) = tryLock hs sc in
624 (sc', scl) = tryLock hs sc in
615 (Bind n (Let ty' val') sc', tyl && vall && scl)
625 (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)
617 = let (bt', btl) = tryLock hs (binderTy b)
627 = let (bt', btl) = tryLock hs (binderTy b)
618 (val', vall) = tryLock hs val
628 (val', vall) = tryLock hs val
619 (sc', scl) = tryLock hs sc in
629 (sc', scl) = tryLock hs sc in
@@ -895,7 +905,7 @@ keepGiven du (u : us) hs = keepGiven du us hs
895
905
896updateEnv [] e = e
906updateEnv [] e = e
897updateEnv ns [] = []
907updateEnv ns [] = []
898−updateEnv ns ((n, b) : env)
908+updateEnv ns ((n, b) : env)
899 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
909 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
900
910
901updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t
911updateProv 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)
907updateError ns (ElaboratingArg f a env e)
917updateError ns (ElaboratingArg f a env e)
908 = ElaboratingArg f a env (updateError ns e)
918 = ElaboratingArg f a env (updateError ns e)
909updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
919updateError 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)
911 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
921 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
912updateError ns e = e
922updateError ns e = e
913
923
@@ -940,7 +950,7 @@ getProvenance _ = (Nothing, Nothing)
940
950
941setReady (x, y, _, env, err, c, at) = (x, y, True, env, err, c, at)
951setReady (x, y, _, env, err, c, at) = (x, y, True, env, err, c, at)
942
952
943−updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
953+updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
944 -> ([(Name, TT Name)], Fails)
954 -> ([(Name, TT Name)], Fails)
945-- updateProblems ctxt [] ps inj holes = ([], ps)
955-- updateProblems ctxt [] ps inj holes = ([], ps)
946updateProblems ps updates probs = rec 10 updates probs
956updateProblems ps updates probs = rec 10 updates probs
@@ -966,8 +976,8 @@ updateProblems ps updates probs = rec 10 updates probs
966 (lp, rp) = getProvenance err
976 (lp, rp) = getProvenance err
967 err' = updateError ns err
977 err' = updateError ns err
968 env' = updateEnv ns env in
978 env' = updateEnv ns env in
969− if newx || newy || ready ||
979+ if newx || newy || ready ||
970− any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
980+ any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
971 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
981 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
972 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $
982 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $
973 let v' = filter (\(n, _) -> n `notElem` dont) v in
983 let v' = filter (\(n, _) -> n `notElem` dont) v in
@@ -980,11 +990,11 @@ updateProblems ps updates probs = rec 10 updates probs
980 updateNs ns (x, y, t, env, err, fc, fa)
990 updateNs ns (x, y, t, env, err, fc, fa)
981 = let (x', newx) = updateSolvedTerm' ns x
991 = let (x', newx) = updateSolvedTerm' ns x
982 (y', newy) = updateSolvedTerm' ns y in
992 (y', newy) = updateSolvedTerm' ns y in
983− (x', y', newx || newy,
993+ (x', y', newx || newy,
984 updateEnv ns env, updateError ns err, fc, fa)
994 updateEnv ns env, updateError ns err, fc, fa)
985
995
986-- attempt to solve remaining problems with match_unify
996-- attempt to solve remaining problems with match_unify
987−matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
997+matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
988 -> ([(Name, TT Name)], Fails)
998 -> ([(Name, TT Name)], Fails)
989matchProblems all ps updates probs = up updates probs where
999matchProblems all ps updates probs = up updates probs where
990 hs = holes ps
1000 hs = holes ps
@@ -1085,7 +1095,7 @@ processTactic t ps
1085 -- apply them here
1095 -- apply them here
1086 let ns' = dropGiven (dontunify ps') ns_in (holes ps')
1096 let ns' = dropGiven (dontunify ps') ns_in (holes ps')
1087 let pterm'' = updateSolved ns' (pterm ps')
1097 let pterm'' = updateSolved ns' (pterm ps')
1088− traceWhen (unifylog ps)
1098+ traceWhen (unifylog ps)
1089 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++
1099 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++
1090 "(Toplevel) Dropping holes: " ++ show (map fst ns') ++ "\n" ++
1100 "(Toplevel) Dropping holes: " ++ show (map fst ns') ++ "\n" ++
1091 "Holes were: " ++ show (holes ps')) $
1101 "Holes were: " ++ show (holes ps')) $
@@ -1139,4 +1149,3 @@ process t h = tactic (Just h) (mktac t)
1139 mktac (MoveLast n) = movelast n
1149 mktac (MoveLast n) = movelast n
1140 mktac (UnifyGoal r) = unifyGoal r
1150 mktac (UnifyGoal r) = unifyGoal r
1141 mktac (UnifyTerms x y) = unifyTerms x y
1151 mktac (UnifyTerms x y) = unifyTerms x y
1142−
src/Idris/Core/ProofTerm.hs+31−28
@@ -1,16 +1,20 @@
1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
1+{-|
2−
2+Module : Idris.Core.ProofTerm
3−{- | Implements a proof state, some primitive tactics for manipulating
3+Description : Proof term. implementation and utilities.
4−proofs, and some high level commands for introducing new theorems,
4+Copyright :
5−evaluation/checking inside the proof system, etc.
5+License : BSD3
6+Maintainer : The Idris Community.
6-}
7-}
7
8
9+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
10+module Idris.Core.ProofTerm(
8−module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
11+ ProofTerm, Goal(..), mkProofTerm, getProofTerm
9− resetProofTerm,
12+ , resetProofTerm
10− updateSolved, updateSolvedTerm, updateSolvedTerm',
13+ , updateSolved, updateSolvedTerm, updateSolvedTerm'
11− bound_in, bound_in_term, refocus, updsubst,
14+ , bound_in, bound_in_term, refocus, updsubst
12− Hole, RunTactic',
15+ , Hole, RunTactic'
13− goal, atHole) where
16+ , goal, atHole
17+ ) where
14
18
15import Idris.Core.Typecheck
19import Idris.Core.Typecheck
16import Idris.Core.Evaluate
20import Idris.Core.Evaluate
@@ -72,7 +76,7 @@ rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
72-- are crossed, and the actual binding term.
76-- are crossed, and the actual binding term.
73findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
77findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
74findHole n env t = fh' env Top t where
78findHole 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)
76 | hole h && n == x = Just (path, env, tm)
80 | hole h && n == x = Just (path, env, tm)
77 fh' env path (App Complete _ _) = Nothing
81 fh' env path (App Complete _ _) = Nothing
78 fh' env path (App s f a)
82 fh' env path (App s f a)
@@ -114,7 +118,7 @@ refocus' (Just n) pt@(PT path env tm ups)
114 -- First look for the hole in the proof term as-is
118 -- First look for the hole in the proof term as-is
115 | Just (p', env', tm') <- findHole n env tm
119 | Just (p', env', tm') <- findHole n env tm
116 = PT (replaceTop p' path) env' tm' ups
120 = 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
118 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
122 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
119 = PT p' env' tm' []
123 = PT p' env' tm' []
120 | otherwise = pt
124 | otherwise = pt
@@ -128,7 +132,7 @@ mkProofTerm :: Term -> ProofTerm
128mkProofTerm tm = PT Top [] tm []
132mkProofTerm tm = PT Top [] tm []
129
133
130getProofTerm :: ProofTerm -> Term
134getProofTerm :: ProofTerm -> Term
131−getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)
135+getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)
132
136
133resetProofTerm :: ProofTerm -> ProofTerm
137resetProofTerm :: ProofTerm -> ProofTerm
134resetProofTerm = mkProofTerm . getProofTerm
138resetProofTerm = mkProofTerm . getProofTerm
@@ -183,11 +187,11 @@ updateSolvedTerm' xs x = updateSolved' xs x where
183 if ut then (P nt n ty', True) else (t, False)
187 if ut then (P nt n ty', True) else (t, False)
184 updateSolved' xs t = (t, False)
188 updateSolved' xs t = (t, False)
185
189
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
187 (v', uv) = updateSolved' xs v in
191 (v', uv) = updateSolved' xs v in
188 if ut || uv then (Let t' v', True)
192 if ut || uv then (Let t' v', True)
189 else (b, False)
193 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
191 (v', uv) = updateSolved' xs v in
195 (v', uv) = updateSolved' xs v in
192 if ut || uv then (Guess t' v', True)
196 if ut || uv then (Guess t' v', True)
193 else (b, False)
197 else (b, False)
@@ -261,7 +265,7 @@ updateSolvedPath ns t@(AppL Complete _ _) = t
261updateSolvedPath ns t@(AppR Complete _ _) = t
265updateSolvedPath ns t@(AppR Complete _ _) = t
262updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)
266updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)
263updateSolvedPath ns (AppR s l p) = AppR s (updateSolvedTerm ns l) (updateSolvedPath ns p)
267updateSolvedPath 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)
265 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
269 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
266 where
270 where
267 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
271 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
@@ -277,18 +281,18 @@ updateSolvedPath ns (InScope n (Hole ty) t)
277updateSolvedPath ns (InScope n b sc)
281updateSolvedPath ns (InScope n b sc)
278 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
282 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
279
283
280−updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
284+updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
281−updateSolved xs pt@(PT path env sub ups)
285+updateSolved xs pt@(PT path env sub ups)
282− = PT path -- (updateSolvedPath xs path)
286+ = PT path -- (updateSolvedPath xs path)
283− (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
287+ (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
284− (updateSolvedTerm xs sub)
288+ (updateSolvedTerm xs sub)
285 (ups ++ xs)
289 (ups ++ xs)
286
290
287goal :: Hole -> ProofTerm -> TC Goal
291goal :: Hole -> ProofTerm -> TC Goal
288−goal h pt@(PT path env sub ups)
292+goal h pt@(PT path env sub ups)
289-- | OK ginf <- g env sub = return ginf
293-- | OK ginf <- g env sub = return ginf
290 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
294 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
291− where
295+ where
292 g :: Env -> Term -> TC Goal
296 g :: Env -> Term -> TC Goal
293 g env (Bind n b@(Guess _ _) sc)
297 g env (Bind n b@(Guess _ _) sc)
294 | same h n = return $ GD env b
298 | same h n = return $ GD env b
@@ -297,7 +301,7 @@ goal h pt@(PT path env sub ups)
297 g env (Bind n b sc) | hole b && same h n = return $ GD env b
301 g env (Bind n b sc) | hole b && same h n = return $ GD env b
298 | otherwise
302 | otherwise
299 = g ((n, b):env) sc `mplus` gb env b
303 = 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"
301 g env (App _ f a) = g env a `mplus` g env f
305 g env (App _ f a) = g env a `mplus` g env f
302 g env t = fail "Can't find hole"
306 g env t = fail "Can't find hole"
303
307
@@ -305,9 +309,9 @@ goal h pt@(PT path env sub ups)
305 gb env (Guess t v) = g env v `mplus` g env t
309 gb env (Guess t v) = g env v `mplus` g env t
306 gb env t = g env (binderTy t)
310 gb env t = g env (binderTy t)
307
311
308−atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
312+atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
309 StateT a TC (ProofTerm, Bool)
313 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)
311 = do let PT path env sub ups = refocus h pt
315 = do let PT path env sub ups = refocus h pt
312 (tm, u) <- atH f c env sub
316 (tm, u) <- atH f c env sub
313 return (PT path env tm ups, u)
317 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
362 bi b = bound_in_term (binderTy b)
366 bi b = bound_in_term (binderTy b)
363bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a
367bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a
364bound_in_term _ = []
368bound_in_term _ = []
365−
src/Idris/Core/TT.hs+39−31
@@ -1,7 +1,11 @@
1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,
1+{-|
2− DeriveDataTypeable, PatternGuards #-}
2+Module : Idris.Core.TT
3−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3+Description : The core language of Idris, TT.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+
4−{-| TT is the core language of Idris. The language has:
8+TT is the core language of Idris. The language has:
5
9
6 * Full dependent types
10 * Full dependent types
7
11
@@ -18,30 +22,34 @@
18 * We have a simple collection of tactics which we use to elaborate source
22 * We have a simple collection of tactics which we use to elaborate source
19 programs with implicit syntax into fully explicit terms.
23 programs with implicit syntax into fully explicit terms.
20-}
24-}
21−
25+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,
26+ DeriveDataTypeable, PatternGuards #-}
27+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
28+module Idris.Core.TT(
22−module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..),
29+ AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
23− ConstraintFC(..), DataOpt(..), DataOpts(..), Datatype(..),
30+ , ConstraintFC(..), DataOpt(..), DataOpts(..), Datatype(..)
24− Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..),
31+ , Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..)
25− FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..),
32+ , FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..)
26− NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..),
33+ , NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..)
27− Provenance(..), Raw(..), SpecialName(..), TC(..), Term(..),
34+ , Provenance(..), Raw(..), SpecialName(..), TC(..), Term(..)
28− TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..),
35+ , TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..)
29− UConstraint(..), UCs(..), UExp(..), Universe(..),
36+ , UConstraint(..), UCs(..), UExp(..), Universe(..)
30− addAlist, addBinder, addDef, allTTNames, arity, bindAll,
37+ , addAlist, addBinder, addDef, allTTNames, arity, bindAll
31− bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact,
38+ , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact
32− discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname,
39+ , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname
33− fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv,
40+ , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv
34− freeNames, getArgTys, getRetTy, implicitable, instantiate,
41+ , freeNames, getArgTys, getRetTy, implicitable, instantiate
35− intTyName, isInjective, isTypeConst, liftPats, lookupCtxt,
42+ , intTyName, isInjective, isTypeConst, liftPats, lookupCtxt
36− lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth,
43+ , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth
37− nextName, noOccurrence, nsroot, occurrences, orderPats,
44+ , nextName, noOccurrence, nsroot, occurrences, orderPats
38− pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV,
45+ , pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV
39− pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget,
46+ , pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget
40− safeForgetEnv, showCG, showEnv, showEnvDbg, showSep,
47+ , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep
41− sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm,
48+ , sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm
42− substV, sUN, tcname, termSmallerThan, tfail, thead, tnull,
49+ , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull
43− toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,
50+ , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName
44− uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm) where
51+ , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm
52+ ) where
45
53
46-- Work around AMP without CPP
54-- Work around AMP without CPP
47import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,
55import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,
@@ -317,7 +325,7 @@ bindTC x k = case x of
317
325
318instance Monad TC where
326instance Monad TC where
319 return x = OK x
327 return x = OK x
320− x >>= k = bindTC x k
328+ x >>= k = bindTC x k
321 fail e = Error (InternalMsg e)
329 fail e = Error (InternalMsg e)
322
330
323instance MonadPlus TC where
331instance MonadPlus TC where
@@ -386,7 +394,7 @@ instance Show Err where
386 show (At f e) = show f ++ ":" ++ show e
394 show (At f e) = show f ++ ":" ++ show e
387 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++
395 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++
388 show x ++ ": " ++ show e
396 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 ++
390 showType ty ++ ":" ++ show e
398 showType ty ++ ":" ++ show e
391 where
399 where
392 showType Nothing = ""
400 showType Nothing = ""
@@ -964,7 +972,7 @@ data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,
964 deriving (Show, Data, Typeable)
972 deriving (Show, Data, Typeable)
965
973
966instance Eq ConstraintFC where
974instance Eq ConstraintFC where
967− x == y = uconstraint x == uconstraint y
975+ x == y = uconstraint x == uconstraint y
968
976
969instance Ord ConstraintFC where
977instance Ord ConstraintFC where
970 compare x y = compare (uconstraint x) (uconstraint y)
978 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+
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
9{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards #-}
10 PatternGuards #-}
3
11
@@ -86,10 +94,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
86 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
94 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
87 -- If we're elaborating, we don't want the private names; if we're
95 -- If we're elaborating, we don't want the private names; if we're
88 -- checking an already elaborated term, we do
96 -- 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
90 = return (P nt n' ty, ty)
98 = return (P nt n' ty, ty)
91 -- If the names are ambiguous, require it to be fully qualified
99 -- 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
93 = return (P nt n' ty, ty)
101 = return (P nt n' ty, ty)
94 | otherwise = do lift $ tfail $ NoSuchVariable n
102 | otherwise = do lift $ tfail $ NoSuchVariable n
95 chk u env ap@(RApp f RType) | not holes
103 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
109 (Bind x (Let (TType v') (TType (UVar v))) t)
117 (Bind x (Let (TType v') (TType (UVar v))) t)
110 return (App Complete fv (TType (UVar v)), apty)
118 return (App Complete fv (TType (UVar v)), apty)
111 Bind x (Pi i s k) t ->
119 Bind x (Pi i s k) t ->
112− do (av, aty) <- chk u env RType
120+ do (av, aty) <- chk u env RType
113 convertsC ctxt env aty s
121 convertsC ctxt env aty s
114 let apty = simplify initContext env
122 let apty = simplify initContext env
115 (Bind x (Let aty av) t)
123 (Bind x (Let aty av) t)
@@ -170,7 +178,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
170 case (normalise ctxt env st, normalise ctxt env tt) of
178 case (normalise ctxt env st, normalise ctxt env tt) of
171 (TType su, TType tu) -> do
179 (TType su, TType tu) -> do
172 when (not holes) $ do (v, cs) <- get
180 when (not holes) $ do (v, cs) <- get
173− put (v, ULE su maxu :
181+ put (v, ULE su maxu :
174 ULE tu maxu : cs)
182 ULE tu maxu : cs)
175 let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u
183 let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u
176 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')
184 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+-}
1{-# LANGUAGE PatternGuards #-}
14{-# LANGUAGE PatternGuards #-}
2
15
16+module Idris.Core.Unify(
17+ match_unify, unify
3−module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..),
18+ , Fails, FailContext(..), FailAt(..)
4− unrecoverable) where
19+ , unrecoverable
20+ ) where
5
21
6import Idris.Core.TT
22import Idris.Core.TT
7import Idris.Core.Evaluate
23import Idris.Core.Evaluate
@@ -12,14 +28,8 @@ import Data.Maybe
12import Data.List
28import Data.List
13import Debug.Trace
29import Debug.Trace
14
30
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−
20-- terms which need to be injective, with the things we're trying to unify
31-- terms which need to be injective, with the things we're trying to unify
21-- at the time
32-- at the time
22−
23data FailAt = Match | Unify
33data FailAt = Match | Unify
24 deriving (Show, Eq)
34 deriving (Show, Eq)
25
35
@@ -62,14 +72,14 @@ cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
62-- Solve metavariables by matching terms against each other
72-- Solve metavariables by matching terms against each other
63-- Not really unification, of course!
73-- Not really unification, of course!
64
74
65−match_unify :: Context -> Env ->
75+match_unify :: Context -> Env ->
66− (TT Name, Maybe Provenance) ->
76+ (TT Name, Maybe Provenance) ->
67 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
77 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
68 TC [(Name, TT Name)]
78 TC [(Name, TT Name)]
69match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
79match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
70 case runStateT (un [] (renameBindersTm env topx)
80 case runStateT (un [] (renameBindersTm env topx)
71 (renameBindersTm env topy)) (UI 0 []) of
81 (renameBindersTm env topy)) (UI 0 []) of
72− OK (v, UI _ []) ->
82+ OK (v, UI _ []) ->
73 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
83 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
74 return (map (renameBinders env) v')
84 return (map (renameBinders env) v')
75 res ->
85 res ->
@@ -136,10 +146,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
136 let r = recoverable (normalise ctxt env (binderTy x))
146 let r = recoverable (normalise ctxt env (binderTy x))
137 (normalise ctxt env (binderTy y))
147 (normalise ctxt env (binderTy y))
138 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
148 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
139− (CantUnify r (binderTy x, Nothing)
149+ (CantUnify r (binderTy x, Nothing)
140 (binderTy y, Nothing) (Msg "") (errEnv env) s)
150 (binderTy y, Nothing) (Msg "") (errEnv env) s)
141 (errEnv env) s
151 (errEnv env) s
142− put (UI s ((binderTy x, binderTy y,
152+ put (UI s ((binderTy x, binderTy y,
143 False,
153 False,
144 env, err, from, Match) : f))
154 env, err, from, Match) : f))
145 return []
155 return []
@@ -236,13 +246,13 @@ trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPa
236 followSols vs ((n, P _ t _) : ns)
246 followSols vs ((n, P _ t _) : ns)
237 | Just t' <- lookup t ns
247 | Just t' <- lookup t ns
238 = do vs' <- case t' of
248 = do vs' <- case t' of
239− P _ tn _ ->
249+ P _ tn _ ->
240 if (n, tn) `elem` vs then -- cycle
250 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)
242 (Msg "") (errEnv env) 0)
252 (Msg "") (errEnv env) 0)
243 else return ((n, tn) : vs)
253 else return ((n, tn) : vs)
244 _ -> return vs
254 _ -> return vs
245− followSols vs' ((n, t') : ns)
255+ followSols vs' ((n, t') : ns)
246 followSols vs (n : ns) = do ns' <- followSols vs ns
256 followSols vs (n : ns) = do ns' <- followSols vs ns
247 return $ n : ns'
257 return $ n : ns'
248
258
@@ -260,8 +270,8 @@ hasv (App _ f a) = hasv f || hasv a
260hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
270hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
261hasv _ = False
271hasv _ = False
262
272
263−unify :: Context -> Env ->
273+unify :: Context -> Env ->
264− (TT Name, Maybe Provenance) ->
274+ (TT Name, Maybe Provenance) ->
265 (TT Name, Maybe Provenance) ->
275 (TT Name, Maybe Provenance) ->
266 [Name] -> [Name] -> [Name] -> [FailContext] ->
276 [Name] -> [Name] -> [Name] -> [FailContext] ->
267 TC ([(Name, TT Name)], Fails)
277 TC ([(Name, TT Name)], Fails)
@@ -281,7 +291,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
281 (UI 0 []) of
291 (UI 0 []) of
282 OK (v, UI _ fails) ->
292 OK (v, UI _ fails) ->
283 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
293 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)) $
285 return (map (renameBinders env) v', reverse fails)
295 return (map (renameBinders env) v', reverse fails)
286-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
296-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
287 Error e -> tfail e
297 Error e -> tfail e
@@ -292,7 +302,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
292
302
293 injective (P (DCon _ _ _) _ _) = True
303 injective (P (DCon _ _ _) _ _) = True
294 injective (P (TCon _ _) _ _) = True
304 injective (P (TCon _ _) _ _) = True
295− injective (P Ref n _)
305+ injective (P Ref n _)
296 | Just i <- lookupInjectiveExact n ctxt = i
306 | Just i <- lookupInjectiveExact n ctxt = i
297 injective (App _ f a) = injective f -- && injective a
307 injective (App _ f a) = injective f -- && injective a
298 injective _ = False
308 injective _ = False
@@ -410,8 +420,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
410 all rigid args,
420 all rigid args,
411 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
421 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
412 -- && TODO: tm does not refer to any variables other than those
422 -- && TODO: tm does not refer to any variables other than those
413− -- in 'args'
423+ -- in 'args'
414− = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
424+ = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
415 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))
425 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))
416 where rigid (V i) = True
426 where rigid (V i) = True
417 rigid (P _ t _) = t `elem` map fst env &&
427 rigid (P _ t _) = t `elem` map fst env &&
@@ -425,14 +435,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
425 getname _ = Nothing
435 getname _ = Nothing
426
436
427 containsOnly args vs (V i) = i `elem` vs
437 containsOnly args vs (V i) = i `elem` vs
428− containsOnly args vs (P Bound n ty)
438+ containsOnly args vs (P Bound n ty)
429 = n `elem` args && containsOnly args vs ty
439 = n `elem` args && containsOnly args vs ty
430− containsOnly args vs (P _ n ty)
440+ containsOnly args vs (P _ n ty)
431 = not (holeIn env n || n `elem` holes)
441 = not (holeIn env n || n `elem` holes)
432 && containsOnly args vs ty
442 && containsOnly args vs ty
433− containsOnly args vs (App _ f a)
443+ containsOnly args vs (App _ f a)
434 = containsOnly args vs f && containsOnly args vs a
444 = containsOnly args vs f && containsOnly args vs a
435− containsOnly args vs (Bind _ b sc)
445+ containsOnly args vs (Bind _ b sc)
436 = containsOnly args vs (binderTy b) &&
446 = containsOnly args vs (binderTy b) &&
437 containsOnly args (0 : map (+1) vs) sc
447 containsOnly args (0 : map (+1) vs) sc
438 containsOnly args vs _ = True
448 containsOnly args vs _ = True
@@ -440,14 +450,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
440 bindLams [] tm = tm
450 bindLams [] tm = tm
441 bindLams (a : as) tm = bindLam a (bindLams as tm)
451 bindLams (a : as) tm = bindLam a (bindLams as tm)
442
452
443− bindLam (V i) tm = Bind (fst (env !! i))
453+ bindLam (V i) tm = Bind (fst (env !! i))
444− (Lam (binderTy (snd (env !! i))))
454+ (Lam (binderTy (snd (env !! i))))
445 tm
455 tm
446 bindLam (P _ n ty) tm = Bind n (Lam ty) tm
456 bindLam (P _ n ty) tm = Bind n (Lam ty) tm
447 bindLam _ tm = error "Can't happen [non rigid bindLam]"
457 bindLam _ tm = error "Can't happen [non rigid bindLam]"
448
458
449 substEnv [] tm = tm
459 substEnv [] tm = tm
450− substEnv ((n, t) : env) tm
460+ substEnv ((n, t) : env) tm
451 = substEnv env (substV (P Bound n (binderTy t)) tm)
461 = substEnv env (substV (P Bound n (binderTy t)) tm)
452
462
453 -- remove any unnecessary lambdas (helps with type class
463 -- remove any unnecessary lambdas (helps with type class
@@ -532,7 +542,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
532 let ax' = hnormalise hf ctxt env (substNames hf ax)
542 let ax' = hnormalise hf ctxt env (substNames hf ax)
533 let ay' = hnormalise hf ctxt env (substNames hf ay)
543 let ay' = hnormalise hf ctxt env (substNames hf ay)
534 -- Don't normalise if we don't have to
544 -- 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)
536 (substNames hf ay))
546 (substNames hf ay))
537 (un' env False bnames ax' ay')
547 (un' env False bnames ax' ay')
538 sc 1
548 sc 1
@@ -607,7 +617,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
607 = do UI s f <- get
617 = do UI s f <- get
608 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
618 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
609 let err = cantUnify from r
619 let err = cantUnify from r
610− (topx, xfrom) (topy, yfrom)
620+ (topx, xfrom) (topy, yfrom)
611 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
621 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
612 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
622 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
613 return []
623 return []
@@ -616,7 +626,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
616 unifyFail x y = do UI s f <- get
626 unifyFail x y = do UI s f <- get
617 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
627 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
618 let err = cantUnify from r
628 let err = cantUnify from r
619− (topx, xfrom) (topy, yfrom)
629+ (topx, xfrom) (topy, yfrom)
620 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
630 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
621 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
631 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
622 lift $ tfail err
632 lift $ tfail err
@@ -636,14 +646,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
636 uB env bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' env False bnames tx ty
646 uB env bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' env False bnames tx ty
637 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
647 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
638 uB env bnames (PVar tx) (PVar ty) = un' env False bnames tx ty
648 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
640 = do UI s f <- get
650 = do UI s f <- get
641 let r = recoverable (normalise ctxt env (binderTy x))
651 let r = recoverable (normalise ctxt env (binderTy x))
642 (normalise ctxt env (binderTy y))
652 (normalise ctxt env (binderTy y))
643 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
653 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
644 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
654 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
645 (errEnv env) s
655 (errEnv env) s
646− put (UI s ((binderTy x, binderTy y,
656+ put (UI s ((binderTy x, binderTy y,
647 False,
657 False,
648 env, err, from, Unify) : f))
658 env, err, from, Unify) : f))
649 return [] -- lift $ tfail err
659 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+
1{-# LANGUAGE PatternGuards #-}
9{-# LANGUAGE PatternGuards #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−
4−-- | Reduction to Weak Head Normal Form
5module Idris.Core.WHNF(whnf, WEnv) where
11module Idris.Core.WHNF(whnf, WEnv) where
6
12
7import Idris.Core.TT
13import Idris.Core.TT
8import Idris.Core.CaseTree
14import Idris.Core.CaseTree
9import Idris.Core.Evaluate hiding (quote)
15import Idris.Core.Evaluate hiding (quote)
10−import qualified Idris.Core.Evaluate as Evaluate
16+import qualified Idris.Core.Evaluate as Evaluate
11
17
12import Debug.Trace
18import Debug.Trace
13
19
@@ -15,7 +21,7 @@ import Debug.Trace
15-- evaluated in (i.e. it's a thunk)
21-- evaluated in (i.e. it's a thunk)
16type StackEntry = (Term, WEnv)
22type StackEntry = (Term, WEnv)
17data WEnv = WEnv Int -- number of free variables
23data WEnv = WEnv Int -- number of free variables
18− [(Term, WEnv)]
24+ [(Term, WEnv)]
19 deriving Show
25 deriving Show
20
26
21type Stack = [StackEntry]
27type Stack = [StackEntry]
@@ -48,14 +54,14 @@ do_whnf :: Context -> WEnv -> Term -> WHNF
48do_whnf ctxt env tm = eval env [] tm
54do_whnf ctxt env tm = eval env [] tm
49 where
55 where
50 eval :: WEnv -> Stack -> Term -> WHNF
56 eval :: WEnv -> Stack -> Term -> WHNF
51− eval wenv@(WEnv d env) stk (V i)
57+ eval wenv@(WEnv d env) stk (V i)
52 | i < length env = let (tm, env') = env !! i in
58 | i < length env = let (tm, env') = env !! i in
53 eval env' stk tm
59 eval env' stk tm
54 | otherwise = error "Can't happen: WHNF scope error"
60 | 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)
56 = eval (WEnv d ((v, wenv) : env)) stk sc
62 = eval (WEnv d ((v, wenv) : env)) stk sc
57 eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)
63 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)
59 = eval (WEnv d ((tm, tenv) : env)) stk sc
65 = eval (WEnv d ((tm, tenv) : env)) stk sc
60
66
61 eval env stk (P nt n ty) = apply env nt n ty stk
67 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
71 eval env stk (UType u) = unload (WUType u) stk
77 eval env stk (UType u) = unload (WUType u) stk
72
78
73 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
79 apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF
74− apply env nt n ty stk
80+ apply env nt n ty stk
75 = let wp = case nt of
81 = let wp = case nt of
76 DCon t a u -> WDCon t a u n (ty, env)
82 DCon t a u -> WDCon t a u n (ty, env)
77 TCon t a -> WTCon t a n (ty, env)
83 TCon t a -> WTCon t a n (ty, env)
@@ -79,12 +85,12 @@ do_whnf ctxt env tm = eval env [] tm
79 _ -> WPRef n (ty, env)
85 _ -> WPRef n (ty, env)
80 in
86 in
81 case lookupDefExact n ctxt of
87 case lookupDefExact n ctxt of
82− Just (CaseOp ci _ _ _ _ cd) ->
88+ Just (CaseOp ci _ _ _ _ cd) ->
83 let (ns, tree) = cases_compiletime cd in
89 let (ns, tree) = cases_compiletime cd in
84 case evalCase env ns tree stk of
90 case evalCase env ns tree stk of
85 Just w -> w
91 Just w -> w
86 Nothing -> unload wp stk
92 Nothing -> unload wp stk
87− Just (Operator _ i op) ->
93+ Just (Operator _ i op) ->
88 if i <= length stk
94 if i <= length stk
89 then case runOp env op (take i stk) (drop i stk) of
95 then case runOp env op (take i stk) (drop i stk) of
90 Just v -> v
96 Just v -> v
@@ -97,7 +103,7 @@ do_whnf ctxt env tm = eval env [] tm
97 unload f (a : as) = unload (WApp f a) as
103 unload f (a : as) = unload (WApp f a) as
98
104
99 runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
105 runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF
100− runOp env op stk rest
106+ runOp env op stk rest
101 = do vals <- mapM tmtoValue stk
107 = do vals <- mapM tmtoValue stk
102 case op vals of
108 case op vals of
103 Just (VConstant c) -> Just $ unload (WConstant c) rest
109 Just (VConstant c) -> Just $ unload (WConstant c) rest
@@ -110,14 +116,14 @@ do_whnf ctxt env tm = eval env [] tm
110 _ -> Nothing
116 _ -> Nothing
111
117
112 tmtoValue :: (Term, WEnv) -> Maybe Value
118 tmtoValue :: (Term, WEnv) -> Maybe Value
113− tmtoValue (tm, tenv)
119+ tmtoValue (tm, tenv)
114 = case eval tenv [] tm of
120 = case eval tenv [] tm of
115 WConstant c -> Just (VConstant c)
121 WConstant c -> Just (VConstant c)
116 _ -> let tm' = quoteEnv tenv tm in
122 _ -> let tm' = quoteEnv tenv tm in
117 Just (toValue ctxt [] tm')
123 Just (toValue ctxt [] tm')
118
124
119 evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
125 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
121 | length ns > length args = Nothing
127 | length ns > length args = Nothing
122 | otherwise = let args' = take (length ns) args
128 | otherwise = let args' = take (length ns) args
123 rest = drop (length ns) args in
129 rest = drop (length ns) args in
@@ -125,25 +131,25 @@ do_whnf ctxt env tm = eval env [] tm
125 let wtm = pToVs (map fst amap) tm
131 let wtm = pToVs (map fst amap) tm
126 Just $ eval (WEnv d (map snd amap)) rest wtm
132 Just $ eval (WEnv d (map snd amap)) rest wtm
127
133
128− evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->
134+ evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->
129 Maybe (Term, [(Name, (Term, WEnv))])
135 Maybe (Term, [(Name, (Term, WEnv))])
130 evalTree env amap (STerm tm) = Just (tm, amap)
136 evalTree env amap (STerm tm) = Just (tm, amap)
131 evalTree env amap (Case _ n alts)
137 evalTree env amap (Case _ n alts)
132 = case lookup n amap of
138 = case lookup n amap of
133− Just (tm, tenv) -> findAlt env amap
139+ Just (tm, tenv) -> findAlt env amap
134 (deconstruct (eval tenv [] tm) []) alts
140 (deconstruct (eval tenv [] tm) []) alts
135 _ -> Nothing
141 _ -> Nothing
136 evalTree _ _ _ = Nothing
142 evalTree _ _ _ = Nothing
137
143
138 deconstruct :: WHNF -> Stack -> (WHNF, Stack)
144 deconstruct :: WHNF -> Stack -> (WHNF, Stack)
139 deconstruct (WApp f arg) stk = deconstruct f (arg : stk)
145 deconstruct (WApp f arg) stk = deconstruct f (arg : stk)
140− deconstruct t stk = (t, stk)
146+ deconstruct t stk = (t, stk)
141
147
142− findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->
148+ findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->
143 [CaseAlt] ->
149 [CaseAlt] ->
144 Maybe (Term, [(Name, (Term, WEnv))])
150 Maybe (Term, [(Name, (Term, WEnv))])
145− findAlt env amap (WDCon tag _ _ _ _, args) alts
151+ findAlt env amap (WDCon tag _ _ _ _, args) alts
146− | Just (ns, sc) <- findTag tag alts
152+ | Just (ns, sc) <- findTag tag alts
147 = let amap' = updateAmap (zip ns args) amap in
153 = let amap' = updateAmap (zip ns args) amap in
148 evalTree env amap' sc
154 evalTree env amap' sc
149 | Just sc <- findDefault alts
155 | Just sc <- findDefault alts
@@ -159,7 +165,7 @@ do_whnf ctxt env tm = eval env [] tm
159 findTag i [] = Nothing
165 findTag i [] = Nothing
160 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
166 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
161 findTag i (_ : xs) = findTag i xs
167 findTag i (_ : xs) = findTag i xs
162−
168+
163 findDefault :: [CaseAlt] -> Maybe SC
169 findDefault :: [CaseAlt] -> Maybe SC
164 findDefault [] = Nothing
170 findDefault [] = Nothing
165 findDefault (DefaultCase sc : xs) = Just sc
171 findDefault (DefaultCase sc : xs) = Just sc
@@ -182,7 +188,7 @@ do_whnf ctxt env tm = eval env [] tm
182quote :: WHNF -> Term
188quote :: WHNF -> Term
183quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
189quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
184quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)
190quote (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)
186quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)
192quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)
187quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
193quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)
188quote (WConstant c) = Constant c
194quote (WConstant c) = Constant c
@@ -195,7 +201,7 @@ quote WImpossible = Impossible
195quoteEnv :: WEnv -> Term -> Term
201quoteEnv :: WEnv -> Term -> Term
196quoteEnv (WEnv d ws) tm = qe' d ws tm
202quoteEnv (WEnv d ws) tm = qe' d ws tm
197 where
203 where
198− qe' d ts (V i)
204+ qe' d ts (V i)
199 | i < d = V i
205 | i < d = V i
200 | otherwise = let (tm, env) = ts !! (i - d) in
206 | otherwise = let (tm, env) = ts !! (i - d) in
201 quoteEnv env tm
207 quoteEnv env tm
@@ -206,4 +212,3 @@ quoteEnv (WEnv d ws) tm = qe' d ws tm
206 qe' d ts (P nt n ty) = P nt n (qe' d ts ty)
212 qe' d ts (P nt n ty) = P nt n (qe' d ts ty)
207 qe' d ts (Proj tm i) = Proj (qe' d ts tm) i
213 qe' d ts (Proj tm i) = Proj (qe' d ts tm) i
208 qe' d ts tm = tm
214 qe' d ts tm = tm
209−
src/Idris/Coverage.hs+8−3
@@ -1,6 +1,11 @@
1−{-# LANGUAGE PatternGuards #-}
1+{-|
2+Module : Idris.Coverage
2−{-| The coverage and totality checkers for Idris are in this module.
3+Description : The coverage and totality checkers for Idris are in this module.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
3-}
7-}
8+{-# LANGUAGE PatternGuards #-}
4module Idris.Coverage where
9module Idris.Coverage where
5
10
6import Idris.Core.TT
11import Idris.Core.TT
@@ -352,7 +357,7 @@ checkPositive mut_ns (cn, ty')
352 where
357 where
353 args t = [0..length (getArgTys t)-1]
358 args t = [0..length (getArgTys t)-1]
354
359
355− cp i (Bind n (Pi _ aty _) sc)
360+ cp i (Bind n (Pi _ aty _) sc)
356 = posArg i aty && cp i sc
361 = posArg i aty && cp i sc
357 cp i t | (P _ n' _ , args) <- unApply t,
362 cp i t | (P _ n' _ , args) <- unApply t,
358 n' `elem` mut_ns = all noRec args
363 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+
1{-# LANGUAGE PatternGuards #-}
9{-# LANGUAGE PatternGuards #-}
2
10
3module Idris.DSL where
11module Idris.DSL where
@@ -16,7 +24,7 @@ debindApp :: SyntaxInfo -> PTerm -> PTerm
16debindApp syn t = debind (dsl_bind (dsl_info syn)) t
24debindApp syn t = debind (dsl_bind (dsl_info syn)) t
17
25
18dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
26dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
19−dslify syn i = transform dslifyApp
27+dslify syn i = transform dslifyApp
20 where
28 where
21 dslifyApp (PApp fc (PRef _ _ f) [a])
29 dslifyApp (PApp fc (PRef _ _ f) [a])
22 | [d] <- lookupCtxt f (idris_dsls i)
30 | [d] <- lookupCtxt f (idris_dsls i)
@@ -225,5 +233,3 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
225 bindAll [] tm = tm
233 bindAll [] tm = tm
226 bindAll ((n, fc, t) : bs) tm
234 bindAll ((n, fc, t) : bs) tm
227 = PApp fc b [pexp t, pexp (PLam fc n NoFC Placeholder (bindAll bs tm))]
235 = 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2
9
3module Idris.DataOpts(applyOpts) where
10module Idris.DataOpts(applyOpts) where
4
11
5−-- Forcing, detagging and collapsing
6−
7import Idris.AbsSyntax
12import Idris.AbsSyntax
8import Idris.AbsSyntaxTree
13import Idris.AbsSyntaxTree
9import Idris.Core.TT
14import 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+-}
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2
9
10+module Idris.DeepSeq(
11+ module Idris.DeepSeq
3−module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where
12+ , module Idris.Core.DeepSeq
13+ ) where
4
14
5import Idris.Core.DeepSeq
15import Idris.Core.DeepSeq
6import Idris.Docstrings
16import 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10+module Idris.Delaborate (
11+ annName, bugaddr, delab, delab', delabMV, delabSugared
3−module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabSugared, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab, pprintDelabTy, pprintErr, resugar) where
12+ , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab
4−
13+ , pprintDelabTy, pprintErr, resugar
5−-- Convert core TT back into high level syntax, primarily for display
14+ ) where
6−-- purposes.
7
15
8import Util.Pretty
16import Util.Pretty
9
17
@@ -253,12 +261,12 @@ pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
253pprintProv i e ExpectedType = text "Expected type"
261pprintProv i e ExpectedType = text "Expected type"
254pprintProv i e InferredVal = text "Inferred value"
262pprintProv i e InferredVal = text "Inferred value"
255pprintProv i e GivenVal = text "Given value"
263pprintProv i e GivenVal = text "Given value"
256−pprintProv i e (SourceTerm tm)
264+pprintProv i e (SourceTerm tm)
257− = text "Type of " <>
265+ = text "Type of " <>
258 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
266 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
259 (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
267 (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
260−pprintProv i e (TooManyArgs tm)
268+pprintProv i e (TooManyArgs tm)
261− = text "Is " <>
269+ = text "Is " <>
262 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
270 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)
263 (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
271 (pprintTerm' i (zip (map fst e) (repeat False)) (delabSugared i tm))
264 <> text " applied to too many arguments?"
272 <> text " applied to too many arguments?"
@@ -277,14 +285,14 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
277 (x, y) = addImplicitDiffs (delabSugared i x_ns) (delabSugared i y_ns) in
285 (x, y) = addImplicitDiffs (delabSugared i x_ns) (delabSugared i y_ns) in
278 text "Type mismatch between" <> indented (annTm x_ns
286 text "Type mismatch between" <> indented (annTm x_ns
279 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
287 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
280− ++ zip nms (repeat False)) x))
288+ ++ zip nms (repeat False)) x))
281 <> case xprov of
289 <> case xprov of
282 Nothing -> empty
290 Nothing -> empty
283 Just t -> text " (" <> pprintProv i sc t <> text ")"
291 Just t -> text " (" <> pprintProv i sc t <> text ")"
284 <$>
292 <$>
285 text "and" <> indented (annTm y_ns
293 text "and" <> indented (annTm y_ns
286 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
294 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
287− ++ zip nms (repeat False)) y))
295+ ++ zip nms (repeat False)) y))
288 <> case yprov of
296 <> case yprov of
289 Nothing -> empty
297 Nothing -> empty
290 Just t -> text " (" <> pprintProv i sc t <> text ")"
298 Just t -> text " (" <> pprintProv i sc t <> text ")"
@@ -301,7 +309,7 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
301 else empty
309 else empty
302pprintErr' i (CantConvert x_in y_in env) =
310pprintErr' i (CantConvert x_in y_in env) =
303 let (x_ns, y_ns, nms) = renameMNs x_in y_in
311 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))
305 (delabSugared i (flagUnique y_ns)) in
313 (delabSugared i (flagUnique y_ns)) in
306 text "Type mismatch between" <>
314 text "Type mismatch between" <>
307 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
315 indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
@@ -346,14 +354,14 @@ pprintErr' i (NotInjective p x y) =
346 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delabSugared i p)) <+>
354 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delabSugared i p)) <+>
347 text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>
355 text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>
348 annTm y (pprintTerm i (delabSugared i y))
356 annTm y (pprintTerm i (delabSugared i y))
349−pprintErr' i (CantResolve _ c e)
357+pprintErr' i (CantResolve _ c e)
350 = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)
358 = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)
351 <>
359 <>
352 case e of
360 case e of
353 Msg "" -> empty
361 Msg "" -> empty
354 _ -> line <> line <> text "Possible cause:" <>
362 _ -> line <> line <> text "Possible cause:" <>
355 indented (pprintErr' i e)
363 indented (pprintErr' i e)
356−pprintErr' i (InvalidTCArg n t)
364+pprintErr' i (InvalidTCArg n t)
357 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "
365 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "
358 <> annName n <$>
366 <> annName n <$>
359 text "(Implementation arguments must be injective)"
367 text "(Implementation arguments must be injective)"
@@ -367,13 +375,13 @@ pprintErr' i (WithFnType ty) =
367 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
375 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
368pprintErr' i (CantMatch t) =
376pprintErr' i (CantMatch t) =
369 text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))
377 text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))
370−pprintErr' i (IncompleteTerm t)
378+pprintErr' i (IncompleteTerm t)
371 = let missing = getMissing [] [] t in
379 = let missing = getMissing [] [] t in
372 case missing of
380 case missing of
373 [] -> text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
381 [] -> text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
374− _ -> align (cat (punctuate (comma <> space)
382+ _ -> align (cat (punctuate (comma <> space)
375 (map pprintIncomplete (nub $ getMissing [] [] t))))
383 (map pprintIncomplete (nub $ getMissing [] [] t))))
376− where
384+ where
377 pprintIncomplete (tm, arg)
385 pprintIncomplete (tm, arg)
378 | expname arg
386 | expname arg
379 = text "Can't infer explicit argument to" <+>
387 = text "Can't infer explicit argument to" <+>
@@ -396,7 +404,7 @@ pprintErr' i (IncompleteTerm t)
396 getMissing hs env (Bind n (Guess _ _) sc)
404 getMissing hs env (Bind n (Guess _ _) sc)
397 = getMissing (n : hs) (n : env) sc
405 = getMissing (n : hs) (n : env) sc
398 getMissing hs env (Bind n (Let t v) sc)
406 getMissing hs env (Bind n (Let t v) sc)
399− = getMissing hs env t ++
407+ = getMissing hs env t ++
400 getMissing hs env v ++
408 getMissing hs env v ++
401 getMissing hs (n : env) sc
409 getMissing hs (n : env) sc
402 getMissing hs env (Bind n b sc)
410 getMissing hs env (Bind n b sc)
@@ -408,7 +416,7 @@ pprintErr' i (IncompleteTerm t)
408 getMissingArgs n [] = []
416 getMissingArgs n [] = []
409 getMissingArgs n (V i : as)
417 getMissingArgs n (V i : as)
410 | env!!i `elem` hs = (n, env!!i) : getMissingArgs n as
418 | env!!i `elem` hs = (n, env!!i) : getMissingArgs n as
411− getMissingArgs n (P _ a _ : as)
419+ getMissingArgs n (P _ a _ : as)
412 | a `elem` hs = (n, a) : getMissingArgs n as
420 | a `elem` hs = (n, a) : getMissingArgs n as
413 getMissingArgs n (a : as) = getMissing hs env a ++ getMissingArgs n as
421 getMissingArgs n (a : as) = getMissing hs env a ++ getMissingArgs n as
414 getMissing hs env (App _ f a)
422 getMissing hs env (App _ f a)
@@ -447,11 +455,11 @@ pprintErr' i (ProofSearchFail e) = pprintErr' i e
447pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))
455pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delabSugared i tm))
448pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
456pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
449pprintErr' i (Elaborating s n ty e) = text "When checking" <+> text s <>
457pprintErr' i (Elaborating s n ty e) = text "When checking" <+> text s <>
450− annName' n (showqual i n) <>
458+ annName' n (showqual i n) <>
451 pprintTy ty <$>
459 pprintTy ty <$>
452 pprintErr' i e
460 pprintErr' i e
453 where pprintTy Nothing = colon
461 where pprintTy Nothing = colon
454− pprintTy (Just ty) = text " with expected type" <>
462+ pprintTy (Just ty) = text " with expected type" <>
455 indented (annTm ty (pprintTerm i (delabSugared i ty)))
463 indented (annTm ty (pprintTerm i (delabSugared i ty)))
456 <> line
464 <> line
457pprintErr' i (ElaboratingArg f x _ e)
465pprintErr' i (ElaboratingArg f x _ e)
@@ -540,12 +548,12 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y
540 where
548 where
541 getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
549 getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
542 getRenames acc [] = return acc
550 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
544 = do idx <- get
552 = do idx <- get
545 put (idx + 1)
553 put (idx + 1)
546 let x' = sUN (str x ++ show idx)
554 let x' = sUN (str x ++ show idx)
547 getRenames ((n, x') : acc) xs
555 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
549 = do idx <- get
557 = do idx <- get
550 put (idx + 1)
558 put (idx + 1)
551 let x' = sUN (str x ++ show idx)
559 let x' = sUN (str x ++ show idx)
@@ -697,4 +705,3 @@ showbasic (MN _ s) = str s
697showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
705showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
698showbasic (SN s) = show s
706showbasic (SN s) = show s
699showbasic n = show n
707showbasic 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+-}
2module Idris.Directives(directiveAction) where
8module Idris.Directives(directiveAction) where
3
9
4import Idris.AbsSyntax
10import 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+-}
1{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}
8{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10+module Idris.Docs (
11+ pprintDocs
3−module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, pprintTypeDoc, FunDoc, FunDoc'(..), Docs, Docs'(..)) where
12+ , getDocs, pprintConstDocs, pprintTypeDoc
13+ , FunDoc, FunDoc'(..), Docs, Docs'(..)
14+ ) where
4
15
5import Idris.AbsSyntax
16import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
17import Idris.AbsSyntaxTree
@@ -149,7 +160,7 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct
149 vsep (map dumpInstance superclasses)))
160 vsep (map dumpInstance superclasses)))
150 where
161 where
151 params' = zip pNames (repeat False)
162 params' = zip pNames (repeat False)
152−
163+
153 (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)
164 (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)
154 instances
165 instances
155
166
@@ -318,7 +329,7 @@ docClass n ci
318 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)
329 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)
319 namedInst n@(UN _) = Just n
330 namedInst n@(UN _) = Just n
320 namedInst _ = Nothing
331 namedInst _ = Nothing
321−
332+
322 getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
333 getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
323 getDInst _ = Nothing
334 getDInst _ = Nothing
324
335
@@ -380,4 +391,4 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty
380
391
381pprintTypeDoc :: IState -> Doc OutputAnnotation
392pprintTypeDoc :: IState -> Doc OutputAnnotation
382pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>
393pprintTypeDoc 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+
1{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}
9{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−
4−-- | Wrapper around Markdown library
5module Idris.Docstrings (
11module Idris.Docstrings (
6− Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,
12+ Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring
13+ , emptyDocstring, nullDocstring, noDocs, overview, containsText
7− overview, containsText, renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring
14+ , renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring
8 ) where
15 ) where
9
16
10import qualified Cheapskate as C
17import 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+-}
1module Idris.Elab.AsPat(desugarAs) where
8module Idris.Elab.AsPat(desugarAs) where
2
9
3import Idris.Core.TT
10import Idris.Core.TT
@@ -30,7 +37,7 @@ collectAs (PApp fc t as)
30 return (PApp fc t as') -- only valid on args
37 return (PApp fc t as') -- only valid on args
31-- only for 'ExactlyOne' since it means the alternatives will have the
38-- only for 'ExactlyOne' since it means the alternatives will have the
32-- same form, so we can assume we only need to extract from the first one
39-- 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))
34 = do a' <- collectAs a
41 = do a' <- collectAs a
35 pats <- get
42 pats <- get
36 as' <- mapM collectAs as -- just to drop the '@'
43 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2{-# OPTIONS_GHC -fwarn-missing-signatures #-}
9{-# OPTIONS_GHC -fwarn-missing-signatures #-}
3module Idris.Elab.Class(elabClass) where
10module 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Clause where
9module Idris.Elab.Clause where
3
10
@@ -1049,13 +1056,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
1049 getApp [] = Nothing
1056 getApp [] = Nothing
1050 currentFn _ tm = tm
1057 currentFn _ tm = tm
1051
1058
1052− updateApp wtm@(PWithApp fcw tm_in warg) =
1059+ updateApp wtm@(PWithApp fcw tm_in warg) =
1053 let tm = currentFn fname tm_in in
1060 let tm = currentFn fname tm_in in
1054 case matchClause ist toplhs tm of
1061 case matchClause ist toplhs tm of
1055 Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))
1062 Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))
1056− Right mvars ->
1063+ Right mvars ->
1057 let ns = map (keepMvar (map fst mvars) fcw) ns_in
1064 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'
1059 wty = lookupTyExact wname (tt_ctxt ist)
1066 wty = lookupTyExact wname (tt_ctxt ist)
1060 res = substMatches mvars $
1067 res = substMatches mvars $
1061 PApp fcw (PRef fcw [] wname)
1068 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Data(elabData) where
9module Idris.Elab.Data(elabData) where
3
10
@@ -206,7 +213,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
206 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
213 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
207 tyIs con t | (P Bound n' _, _) <- unApply t
214 tyIs con t | (P Bound n' _, _) <- unApply t
208 = if n' /= tn then
215 = if n' /= tn then
209− tclift $ tfail (At fc (Elaborating "constructor " con Nothing
216+ tclift $ tfail (At fc (Elaborating "constructor " con Nothing
210 (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))
217 (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))
211 else return ()
218 else return ()
212 tyIs con t | (P _ n' _, _) <- unApply t
219 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Instance(elabInstance) where
9module Idris.Elab.Instance(elabInstance) where
3
10
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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Provider(elabProvider) where
9module Idris.Elab.Provider(elabProvider) where
3
10
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+-}
1module Idris.Elab.Quasiquote (extractUnquotes) where
8module Idris.Elab.Quasiquote (extractUnquotes) where
2
9
3import Idris.Core.Elaborate hiding (Tactic(..))
10import 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+-}
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
8{-# LANGUAGE PatternGuards, ViewPatterns #-}
2module Idris.Elab.Record(elabRecord) where
9module Idris.Elab.Record(elabRecord) where
3
10
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+-}
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
8{-# LANGUAGE PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
10module 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+-}
1module Idris.Elab.RunElab (elabRunElab) where
8module Idris.Elab.RunElab (elabRunElab) where
2
9
3import Idris.Elab.Term
10import 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+-}
1{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
8{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Elab.Term where
10module Idris.Elab.Term where
@@ -1664,7 +1671,7 @@ pruneByType env (P _ n _) goalty ist as
1664 case unApply (getRetTy ty') of
1671 case unApply (getRetTy ty') of
1665 (V _, _) ->
1672 (V _, _) ->
1666 isPlausible ist var env n ty
1673 isPlausible ist var env n ty
1667− _ -> matching (getRetTy ty') goalty
1674+ _ -> matching (getRetTy ty') goalty
1668 || isCoercion (getRetTy ty') goalty
1675 || isCoercion (getRetTy ty') goalty
1669-- May be useful to keep for debugging purposes for a bit:
1676-- May be useful to keep for debugging purposes for a bit:
1670-- let res = matching (getRetTy ty') goalty in
1677-- let res = matching (getRetTy ty') goalty in
@@ -1698,7 +1705,7 @@ pruneByType env (P _ n _) goalty ist as
1698 isCoercion rty gty | (P _ r _, _) <- unApply rty
1705 isCoercion rty gty | (P _ r _, _) <- unApply rty
1699 = not (null (getCoercionsBetween r gty))
1706 = not (null (getCoercionsBetween r gty))
1700 isCoercion _ _ = False
1707 isCoercion _ _ = False
1701−
1708+
1702 getCoercionsBetween :: Name -> Type -> [Name]
1709 getCoercionsBetween :: Name -> Type -> [Name]
1703 getCoercionsBetween r goal
1710 getCoercionsBetween r goal
1704 = let cs = getCoercionsTo ist goal in
1711 = let cs = getCoercionsTo ist goal in
@@ -1711,7 +1718,7 @@ pruneByType env (P _ n _) goalty ist as
1711 _ -> [] in
1718 _ -> [] in
1712 ps ++ findCoercions t ns
1719 ps ++ findCoercions t ns
1713
1720
1714− useR ty =
1721+ useR ty =
1715 case unApply (getRetTy ty) of
1722 case unApply (getRetTy ty) of
1716 (P _ t _, _) -> t == r
1723 (P _ t _, _) -> t == r
1717 _ -> False
1724 _ -> 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Transform where
9module Idris.Elab.Transform where
3
10
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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
9+module Idris.Elab.Type (
2−module Idris.Elab.Type (buildType, elabType, elabType',
10+ buildType, elabType, elabType'
3− elabPostulate, elabExtern) where
11+ , elabPostulate, elabExtern
12+ ) where
4
13
5import Idris.AbsSyntax
14import Idris.AbsSyntax
6import Idris.ASTUtils
15import 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Utils where
9module Idris.Elab.Utils where
3
10
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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10+module Idris.Elab.Value(
3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,
11+ elabVal, elabValBind, elabDocTerms
4− elabExec, elabREPL) where
12+ , elabExec, elabREPL
13+ ) where
5
14
6import Idris.AbsSyntax
15import Idris.AbsSyntax
7import Idris.ASTUtils
16import 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+
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
9{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards #-}
10 PatternGuards #-}
3
11
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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2
9
3module Idris.Erasure (performUsageAnalysis, mkFieldName) where
10module Idris.Erasure (performUsageAnalysis, mkFieldName) where
@@ -54,7 +61,7 @@ type DepSet = Map Node (Set Reason)
54-- "function f uses the argument i".
61-- "function f uses the argument i".
55type Cond = Set Node
62type Cond = Set Node
56
63
57−-- ^ Variables carry certain information with them.
64+-- | Variables carry certain information with them.
58data VarInfo = VI
65data VarInfo = VI
59 { viDeps :: DepSet -- ^ dependencies drawn in by the variable
66 { viDeps :: DepSet -- ^ dependencies drawn in by the variable
60 , viFunArg :: Maybe Int -- ^ which function argument this variable came from (defined only for patvars)
67 , 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2
9
3module Idris.ErrReverse(errReverse) where
10module 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+-}
1{-# LANGUAGE DeriveDataTypeable #-}
8{-# LANGUAGE DeriveDataTypeable #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3
10
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+
1module Idris.Help (CmdArg(..), extraHelp) where
9module Idris.Help (CmdArg(..), extraHelp) where
2
10
3data CmdArg = ExprArg -- ^ The command takes an expression
11data 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+-}
1{-# LANGUAGE TypeSynonymInstances #-}
8{-# LANGUAGE TypeSynonymInstances #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3
10
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+-}
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2
9
3{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
10{-# 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2{-# LANGUAGE OverloadedStrings #-}
9{-# LANGUAGE OverloadedStrings #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4−
5−-- | Generation of HTML documentation for Idris code
6module Idris.IdrisDoc (generateDocs) where
11module Idris.IdrisDoc (generateDocs) where
7
12
8import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),
13import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),
src/Idris/Imports.hs+11−2
@@ -1,5 +1,14 @@
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(
1−module Idris.Imports(IFileType(..), findImport, findInPath, findPkgIndex,
9+ IFileType(..), findImport, findInPath, findPkgIndex
2− ibcPathNoFallback, installedPackages, pkgIndex) where
10+ , ibcPathNoFallback, installedPackages, pkgIndex
11+ ) where
3
12
4import Control.Applicative ((<$>))
13import Control.Applicative ((<$>))
5import Data.List (isSuffixOf)
14import 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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2
9
3module Idris.Inliner(inlineDef, inlineTerm) where
10module 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+-}
2
8
3−module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
9+{-# LANGUAGE PatternGuards #-}
4− addMissing, makeWith, makeCase, doProofSearch,
5− makeLemma) where
6
10
7−{- Bits and pieces for editing source files interactively, called from
11+module Idris.Interactive(
8− the REPL -}
12+ caseSplitAt, addClauseFrom, addProofClauseFrom
13+ , addMissing, makeWith, makeCase, doProofSearch
14+ , makeLemma
15+ ) where
9
16
10import Idris.Core.TT
17import Idris.Core.TT
11import Idris.Core.Evaluate
18import 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+
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2
10
3module Idris.Output where
11module Idris.Output where
@@ -99,7 +107,7 @@ iPrintFunTypes bnd n overloads = do ist <- getIState
99 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
107 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
100 iRenderResult output
108 iRenderResult output
101 where fullName ppo n | length overloads > 1 = prettyName True True bnd n
109 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
103 ppOverload ppo infixes n tm =
111 ppOverload ppo infixes n tm =
104 fullName ppo n <+> colon <+> align tm
112 fullName ppo n <+> colon <+> align tm
105
113
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+-}
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
8{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2{-# OPTIONS_GHC -O0 #-}
9{-# OPTIONS_GHC -O0 #-}
3module Idris.Parser(module Idris.Parser,
10module Idris.Parser(module Idris.Parser,
@@ -797,7 +804,7 @@ openInterface syn =
797 <?> "open interface declaration"
804 <?> "open interface declaration"
798
805
799
806
800−
807+
801
808
802
809
803{-| Parses a mutual declaration (for mutually recursive functions)
810{-| 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+-}
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
8{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.Parser.Data where
9module Idris.Parser.Data where
3
10
4import Prelude hiding (pi)
11import Prelude hiding (pi)
5
12
6import Text.Trifecta.Delta
13import Text.Trifecta.Delta
7−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)
14+import Text.Trifecta hiding ( span, stringLiteral, charLiteral, natural
15+ , symbol, char, string, whiteSpace, Err)
16+
8−import Text.Parser.LookAhead
17+import Text.Parser.LookAhead
9−import Text.Parser.Expression
18+import Text.Parser.Expression
10import qualified Text.Parser.Token as Tok
19import qualified Text.Parser.Token as Tok
11import qualified Text.Parser.Char as Chr
20import qualified Text.Parser.Char as Chr
12import qualified Text.Parser.Token.Highlight as Hi
21import qualified Text.Parser.Token.Highlight as Hi
@@ -26,11 +35,11 @@ import Control.Applicative
26import Control.Monad
35import Control.Monad
27import Control.Monad.State.Strict
36import Control.Monad.State.Strict
28
37
29−import Data.Maybe
38+import Data.Maybe
30import qualified Data.List.Split as Spl
39import qualified Data.List.Split as Spl
31−import Data.List
40+import Data.List
32−import Data.Monoid
41+import Data.Monoid
33−import Data.Char
42+import Data.Char
34import qualified Data.HashSet as HS
43import qualified Data.HashSet as HS
35import qualified Data.Text as T
44import qualified Data.Text as T
36import qualified Data.ByteString.UTF8 as UTF8
45import qualified Data.ByteString.UTF8 as UTF8
src/Idris/Parser/Expr.hs+13−5
@@ -1,4 +1,12 @@
1+{-|
2+Module : Idris.Parser.Expr
3+Description : Parse Expressions.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}
8+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds #-}
9+{-# LANGUAGE PatternGuards, TupleSections #-}
2module Idris.Parser.Expr where
10module Idris.Parser.Expr where
3
11
4import Prelude hiding (pi)
12import Prelude hiding (pi)
@@ -80,7 +88,7 @@ expr = pi
80-}
88-}
81opExpr :: SyntaxInfo -> IdrisParser PTerm
89opExpr :: SyntaxInfo -> IdrisParser PTerm
82opExpr syn = do i <- get
90opExpr syn = do i <- get
83− buildExpressionParser (table (idris_infixes i))
91+ buildExpressionParser (table (idris_infixes i))
84 (expr' syn)
92 (expr' syn)
85
93
86{- | Parses either an internally defined expression or
94{- | Parses either an internally defined expression or
@@ -955,8 +963,8 @@ rewriteTerm syn = do kw <- reservedFC "rewrite"
955 fc <- getFC
963 fc <- getFC
956 prf <- expr syn
964 prf <- expr syn
957 giving <- optional (do symbol "==>"; expr' syn)
965 giving <- optional (do symbol "==>"; expr' syn)
958− using <- optional (do reserved "using"
966+ using <- optional (do reserved "using"
959− (n, _) <- name
967+ (n, _) <- name
960 return n)
968 return n)
961 kw' <- reservedFC "in"; sc <- expr syn
969 kw' <- reservedFC "in"; sc <- expr syn
962 highlightP kw AnnKeyword
970 highlightP kw AnnKeyword
@@ -1128,7 +1136,7 @@ pi syn =
1128 st <- static
1136 st <- static
1129 explicitPi opts st syn
1137 explicitPi opts st syn
1130 <|> try (do lchar '{'; implicitPi opts st syn)
1138 <|> try (do lchar '{'; implicitPi opts st syn)
1131− <|> if constraintAllowed syn
1139+ <|> if constraintAllowed syn
1132 then try (constraintPi opts st syn)
1140 then try (constraintPi opts st syn)
1133 <|> unboundPi opts st syn
1141 <|> unboundPi opts st syn
1134 else unboundPi opts st syn
1142 else unboundPi opts st syn
src/Idris/Parser/Helpers.hs+9−1
@@ -1,4 +1,12 @@
1+{-|
2+Module : Idris.Parser.Helpers
3+Description : Utilities for Idris' parser.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
1−{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, StandaloneDeriving #-}
8+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds #-}
9+{-# LANGUAGE PatternGuards, StandaloneDeriving #-}
2#if !(MIN_VERSION_base(4,8,0))
10#if !(MIN_VERSION_base(4,8,0))
3{-# LANGUAGE OverlappingInstances #-}
11{-# LANGUAGE OverlappingInstances #-}
4#endif
12#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+-}
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
8{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.Parser.Ops where
9module Idris.Parser.Ops where
3
10
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+-}
1{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
2
9
10+module Idris.PartialEval(
3−module Idris.PartialEval(partial_eval, getSpecApps, specType,
11+ partial_eval, getSpecApps, specType
4− mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),
12+ , mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)
5− pe_app, pe_def, pe_clauses, pe_simple) where
13+ , pe_app, pe_def, pe_clauses, pe_simple
14+ ) where
6
15
7import Idris.AbsSyntax
16import Idris.AbsSyntax
8import Idris.Delaborate
17import 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+-}
1{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
8{-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
2
9
3module Idris.Primitives(primitives, Prim(..)) where
10module 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+
1{-# LANGUAGE PatternGuards #-}
9{-# LANGUAGE PatternGuards #-}
2
10
3−module Idris.ProofSearch(trivial, trivialHoles, proofSearch, resolveTC) where
11+module Idris.ProofSearch(
12+ trivial
13+ , trivialHoles
14+ , proofSearch
15+ , resolveTC
16+ ) where
4
17
5import Idris.Core.Elaborate hiding (Tactic(..))
18import Idris.Core.Elaborate hiding (Tactic(..))
6import Idris.Core.TT
19import 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+-}
2{-# LANGUAGE PatternGuards #-}
8{-# LANGUAGE PatternGuards #-}
3module Idris.Prover (prover, showProof, showRunElab) where
9module Idris.Prover (prover, showProof, showRunElab) where
4
10
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+-}
1{-# LANGUAGE PatternGuards, DeriveFunctor #-}
8{-# LANGUAGE PatternGuards, DeriveFunctor #-}
2−module Idris.Providers (providerTy, getProvided, Provided(..)) where
9+module Idris.Providers (
10+ providerTy
11+ , getProvided
12+ , Provided(..)
13+ ) where
3
14
4import Idris.Core.TT
15import Idris.Core.TT
5import Idris.Core.Evaluate
16import Idris.Core.Evaluate
@@ -39,4 +50,3 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm
39 | otherwise = ifail $ "Internal type provider error: result was not " ++
50 | otherwise = ifail $ "Internal type provider error: result was not " ++
40 "IO (Provider a), or perhaps missing normalisation." ++
51 "IO (Provider a), or perhaps missing normalisation." ++
41 "Term: " ++ take 1000 (show tm)
52 "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+-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards, CPP #-}
9 PatternGuards, CPP #-}
3
10
11+module Idris.REPL(
4−module Idris.REPL(getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc,
12+ getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc
5− getPkgREPL, getPkgTest, getPort, getIBCSubDir,
13+ , getPkgREPL, getPkgTest, getPort, getIBCSubDir
6− idris, idrisMain, loadInputs,
14+ , idris, idrisMain, loadInputs
7− opt, runClient, runMain, ver) where
15+ , opt, runClient, runMain, ver
16+ ) where
8
17
9import Idris.AbsSyntax
18import Idris.AbsSyntax
10import Idris.ASTUtils
19import Idris.ASTUtils
@@ -1457,7 +1466,7 @@ showTotalN :: IState -> Name -> Doc OutputAnnotation
1457showTotalN ist n = case lookupTotal n (tt_ctxt ist) of
1466showTotalN ist n = case lookupTotal n (tt_ctxt ist) of
1458 [t] -> showN n <> text ", which is" <+> showTotal t ist
1467 [t] -> showN n <> text ", which is" <+> showTotal t ist
1459 _ -> empty
1468 _ -> empty
1460− where
1469+ where
1461 ppo = ppOptionIst ist
1470 ppo = ppOptionIst ist
1462 showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
1471 showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
1463 showName (Just ist) [] ppo False n
1472 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+
1{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
2
10
3module Idris.REPL.Browse (namespacesInNS, namesInNS) where
11module Idris.REPL.Browse (namespacesInNS, namesInNS) where
src/Idris/REPL/Parser.hs+13−2
@@ -1,5 +1,16 @@
1−
1+{-|
2+Module : Idris.REPL.Parser
3+Description : Parser for the REPL commands.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
2−module Idris.REPL.Parser (parseCmd, help, allHelp, setOptions) where
8+module Idris.REPL.Parser (
9+ parseCmd
10+ , help
11+ , allHelp
12+ , setOptions
13+ ) where
3
14
4import System.FilePath ((</>))
15import System.FilePath ((</>))
5import System.Console.ANSI (Color(..))
16import System.Console.ANSI (Color(..))
src/Idris/Reflection.hs+8−3
@@ -1,6 +1,11 @@
1+{-|
2+Module : Idris.Reflection
1−{-| Code related to Idris's reflection system. This module contains
3+Description : Code related to Idris's reflection system. This module contains quoters and unquoters along with some supporting datatypes.
2−quoters and unquoters along with some supporting datatypes.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
3-}
7-}
8+
4{-# LANGUAGE PatternGuards, CPP #-}
9{-# LANGUAGE PatternGuards, CPP #-}
5{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
6module Idris.Reflection where
11module Idris.Reflection where
@@ -900,7 +905,7 @@ reflectErr (NotInjective t1 t2 t3) =
900 , reflect t2
905 , reflect t2
901 , reflect t3
906 , reflect t3
902 ]
907 ]
903−reflectErr (CantResolve _ t more)
908+reflectErr (CantResolve _ t more)
904 = raw_apply (Var $ reflErrName "CantResolve") [reflect t, reflectErr more]
909 = raw_apply (Var $ reflErrName "CantResolve") [reflect t, reflectErr more]
905reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
910reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
906reflectErr (CantResolveAlts ss) =
911reflectErr (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+
1{-# LANGUAGE PatternGuards #-}
9{-# LANGUAGE PatternGuards #-}
2
10
3−module Idris.Transforms(transformPats,
11+module Idris.Transforms(
12+ transformPats
4− transformPatsWith,
13+ , transformPatsWith
5− applyTransRulesWith,
14+ , applyTransRulesWith
6− applyTransRules) where
15+ , applyTransRules
16+ ) where
7
17
8import Idris.AbsSyntax
18import Idris.AbsSyntax
9import Idris.Core.CaseTree
19import 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+-}
1{-# LANGUAGE ScopedTypeVariables #-}
8{-# LANGUAGE ScopedTypeVariables #-}
2
9
3module Idris.TypeSearch (
10module Idris.TypeSearch (
11+ searchByType
12+ , searchPred
4− searchByType, searchPred, defaultScoreFunction
13+ , defaultScoreFunction
5−) where
14+ ) where
6
15
7import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))
16import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))
8−import Control.Arrow (first, second, (&&&), (***))
17+import Control.Arrow (first, second, (&&&), (***))
9−import Control.Monad (when, guard)
18+import Control.Monad (when, guard)
10−
19+
11−import Data.List (find, partition, (\\))
20+import Data.List (find, partition, (\\))
12−import Data.Map (Map)
21+import Data.Map (Map)
13−import qualified Data.Map as M
22+import qualified Data.Map as M
14−import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)
23+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)
15−import Data.Monoid (Monoid (mempty, mappend))
24+import Data.Monoid (Monoid (mempty, mappend))
16−import Data.Ord (comparing)
25+import Data.Ord (comparing)
17import qualified Data.PriorityQueue.FingerTree as Q
26import qualified Data.PriorityQueue.FingerTree as Q
18−import Data.Set (Set)
27+import Data.Set (Set)
19−import qualified Data.Set as S
28+import qualified Data.Set as S
20−import qualified Data.Text as T (pack, isPrefixOf)
29+import qualified Data.Text as T (pack, isPrefixOf)
21−import Data.Traversable (traverse)
30+import Data.Traversable (traverse)
22−
31+
23−import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)
32+import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)
24−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,
33+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris
25− IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
34+ , IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
26− implicitAllowed, OutputMode(..), PTerm, toplevel)
35+ implicitAllowed, OutputMode(..), PTerm, toplevel)
27import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
36import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
28−import Idris.Core.TT hiding (score)
37+import Idris.Core.TT hiding (score)
29−import Idris.Core.Unify (match_unify)
38+import Idris.Core.Unify (match_unify)
30−import Idris.Delaborate (delabTy)
39+import Idris.Delaborate (delabTy)
31−import Idris.Docstrings (noDocs, overview)
40+import Idris.Docstrings (noDocs, overview)
32−import Idris.Elab.Type (elabType)
41+import Idris.Elab.Type (elabType)
33−import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)
42+import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)
34import Idris.IBC
43import Idris.IBC
35
44
36import Prelude hiding (pred)
45import Prelude hiding (pred)
@@ -40,9 +49,9 @@ import Util.Pretty (text, char, vsep, (<>), Doc, annotate)
40searchByType :: [String] -> PTerm -> Idris ()
49searchByType :: [String] -> PTerm -> Idris ()
41searchByType pkgs pterm = do
50searchByType pkgs pterm = do
42 i <- getIState -- save original
51 i <- getIState -- save original
43− when (not (null pkgs)) $
52+ when (not (null pkgs)) $
44 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
53 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
45−
54+
46 mapM_ loadPkgIndex pkgs
55 mapM_ loadPkgIndex pkgs
47 pterm' <- addUsingConstraints syn emptyFC pterm
56 pterm' <- addUsingConstraints syn emptyFC pterm
48 pterm'' <- implicit toplevel syn name pterm'
57 pterm'' <- implicit toplevel syn name pterm'
@@ -67,9 +76,9 @@ searchByType pkgs pterm = do
67 name = sMN 0 "searchType" -- name
76 name = sMN 0 "searchType" -- name
68
77
69-- | Conduct a type-directed search using a given match predicate
78-- | 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)])
71 -> IState -> Type -> [(Name, a)]
80 -> 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 $
73 M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
82 M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
74 where
83 where
75 nty = normaliseC ctxt [] ty
84 nty = normaliseC ctxt [] ty
@@ -81,7 +90,7 @@ searchUsing pred istate ty = pred istate nty . concat . M.elems $
81 special :: Name -> Bool
90 special :: Name -> Bool
82 special (NS n _) = special n
91 special (NS n _) = special n
83 special (SN _) = True
92 special (SN _) = True
84− special (UN n) = T.pack "default#" `T.isPrefixOf` n
93+ special (UN n) = T.pack "default#" `T.isPrefixOf` n
85 || n `elem` map T.pack ["believe_me", "really_believe_me"]
94 || n `elem` map T.pack ["believe_me", "really_believe_me"]
86 special _ = False
95 special _ = False
87
96
@@ -117,10 +126,10 @@ reverseDag xs = map f xs where
117
126
118-- run vToP first!
127-- run vToP first!
119-- | Compute a directed acyclic graph corresponding to the
128-- | Compute a directed acyclic graph corresponding to the
120−-- arguments of a function.
129+-- arguments of a function.
121-- returns [(the name and type of the bound variable
130-- returns [(the name and type of the bound variable
122-- the names in the type of the bound variable)]
131-- the names in the type of the bound variable)]
123−computeDagP :: Ord n
132+computeDagP :: Ord n
124 => (TT n -> Bool) -- ^ filter to remove some arguments
133 => (TT n -> Bool) -- ^ filter to remove some arguments
125 -> TT n
134 -> TT n
126 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
135 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
@@ -196,7 +205,7 @@ displayScore score = case both noMods (asymMods score) of
196 Sided True False -> annotated LT "<" -- found type is more general than searched type
205 Sided True False -> annotated LT "<" -- found type is more general than searched type
197 Sided False True -> annotated GT ">" -- searched type is more general than found type
206 Sided False True -> annotated GT ">" -- searched type is more general than found type
198 Sided False False -> text "_"
207 Sided False False -> text "_"
199− where
208+ where
200 annotated ordr = annotate (AnnSearchResult ordr) . text
209 annotated ordr = annotate (AnnSearchResult ordr) . text
201 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
210 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
202
211
@@ -208,19 +217,19 @@ scoreCriterion (Score _ _ amods) = not
208 ( sided (&&) (both ((> 0) . argApp) amods)
217 ( sided (&&) (both ((> 0) . argApp) amods)
209 || sided (+) (both argApp amods) > 4
218 || sided (+) (both argApp amods) > 4
210 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
219 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
211− )
220+ )
212
221
213-- | Convert a 'Score' to an 'Int' to provide an order for search results.
222-- | Convert a 'Score' to an 'Int' to provide an order for search results.
214-- Lower scores are better.
223-- Lower scores are better.
215defaultScoreFunction :: Score -> Int
224defaultScoreFunction :: Score -> Int
216−defaultScoreFunction (Score trans eqFlip amods) =
225+defaultScoreFunction (Score trans eqFlip amods) =
217 trans + eqFlip + linearPenalty + upAndDowncastPenalty
226 trans + eqFlip + linearPenalty + upAndDowncastPenalty
218 where
227 where
219 -- prefer finding a more general type to a less general type
228 -- 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)
221 (both (\(Mods app tcApp tcIntro) -> 3 * app + 4 * tcApp + 2 * tcIntro) amods)
230 (both (\(Mods app tcApp tcIntro) -> 3 * app + 4 * tcApp + 2 * tcIntro) amods)
222 -- it's very bad to have *both* upcasting and downcasting
231 -- it's very bad to have *both* upcasting and downcasting
223− upAndDowncastPenalty = 100 *
232+ upAndDowncastPenalty = 100 *
224 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
233 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
225
234
226instance Ord Score where
235instance Ord Score where
@@ -237,7 +246,7 @@ instance Monoid AsymMods where
237
246
238instance Monoid Score where
247instance Monoid Score where
239 mempty = Score 0 0 mempty
248 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')
241
250
242-- | A directed acyclic graph representing the arguments to a function
251-- | A directed acyclic graph representing the arguments to a function
243-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
252-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
@@ -311,7 +320,7 @@ flipEqualities t = case t of
311 [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]
320 [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]
312 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))
321 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))
313 <$> traverse flipEqualities binder <*> flipEqualities sc
322 <$> 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'))
315 <$> flipEqualities f <*> flipEqualities x
324 <$> flipEqualities f <*> flipEqualities x
316 t' -> [(0, t')]
325 t' -> [(0, t')]
317 where app = App Complete
326 where app = App Complete
@@ -329,13 +338,13 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
329 where
338 where
330 ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))
339 ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))
331 <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2
340 <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2
332− flipEqualitiesDag dag = case dag of
341+ flipEqualitiesDag dag = case dag of
333 [] -> [(0, [])]
342 [] -> [(0, [])]
334− ((n, ty), (pos, deps)) : xs ->
343+ ((n, ty), (pos, deps)) : xs ->
335 (\(i, ty') (j, xs') -> (i + j , ((n, ty'), (pos, deps)) : xs'))
344 (\(i, ty') (j, xs') -> (i + j , ((n, ty'), (pos, deps)) : xs'))
336 <$> flipEqualities ty <*> flipEqualitiesDag xs
345 <$> flipEqualities ty <*> flipEqualitiesDag xs
337 startStates (numEqFlips, sndDag, sndRetTy) = do
346 startStates (numEqFlips, sndDag, sndRetTy) = do
338− state <- unifyQueue (State startingHoles
347+ state <- unifyQueue (State startingHoles
339 (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))
348 (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))
340 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]
349 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]
341 return (score state, state)
350 return (score state, state)
@@ -346,7 +355,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
346 usedns = map fst startingHoles
355 usedns = map fst startingHoles
347 startingHoles = argNames1 ++ argNames2
356 startingHoles = argNames1 ++ argNames2
348
357
349− startingTypes = [(retTy1, retTy2)]
358+ startingTypes = [(retTy1, retTy2)]
350
359
351
360
352 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
361 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
@@ -372,14 +381,14 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
372 (dag1, typeClassArgs1, retTy1) = makeDag type1
381 (dag1, typeClassArgs1, retTy1) = makeDag type1
373 argNames1 = map fst dag1
382 argNames1 = map fst dag1
374 makeDag :: Type -> (ArgsDAG, Classes, Type)
383 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) .
376 computeDagP (isTypeClassArg classInfo) . vToP . unLazy
385 computeDagP (isTypeClassArg classInfo) . vToP . unLazy
377 first3 f (a,b,c) = (f a, b, c)
386 first3 f (a,b,c) = (f a, b, c)
378−
387+
379 -- update our state with the unification resolutions
388 -- update our state with the unification resolutions
380 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
389 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
381 resolveUnis [] state = Just (state, [])
390 resolveUnis [] state = Just (state, [])
382− resolveUnis ((name, term@(P Bound name2 _)) : xs)
391+ resolveUnis ((name, term@(P Bound name2 _)) : xs)
383 state | isJust findArgs = do
392 state | isJust findArgs = do
384 ((ty1, ix1), (ty2, ix2)) <- findArgs
393 ((ty1, ix1), (ty2, ix2)) <- findArgs
385
394
@@ -408,7 +417,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
408 -- due to injectivity
417 -- due to injectivity
409 matchedVarMap = usedVars term
418 matchedVarMap = usedVars term
410 bothT f (x, y) = (f x, f y)
419 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
412 varsInTy = injUsedVars ++ notInjUsedVars
421 varsInTy = injUsedVars ++ notInjUsedVars
413 toDelete = name : varsInTy
422 toDelete = name : varsInTy
414 deleteMany = foldr (.) id (map deleteName toDelete)
423 deleteMany = foldr (.) id (map deleteName toDelete)
@@ -417,7 +426,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
417
426
418 addScore additions theState = theState { score = let s = score theState in
427 addScore additions theState = theState { score = let s = score theState in
419 s { asymMods = asymMods s `mappend` additions } }
428 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
421 , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }
430 , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }
422 nextStep = resolveUnis xs state'
431 nextStep = resolveUnis xs state'
423
432
@@ -427,8 +436,8 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
427 unifyQueue state [] = return state
436 unifyQueue state [] = return state
428 unifyQueue state ((ty1, ty2) : queue) = do
437 unifyQueue state ((ty1, ty2) : queue) = do
429 --trace ("go: \n" ++ show state) True `seq` return ()
438 --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]
439+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]
431− (ty1, Nothing)
440+ (ty1, Nothing)
432 (ty2, Nothing) [] (map fst $ holes state) []
441 (ty2, Nothing) [] (map fst $ holes state) []
433 (state', queueAdditions) <- resolveUnis res state
442 (state', queueAdditions) <- resolveUnis res state
434 guard $ scoreCriterion (score state')
443 guard $ scoreCriterion (score state')
@@ -453,7 +462,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
453 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
462 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
454 nextStepsQueue queue = do
463 nextStepsQueue queue = do
455 ((nextScore, next), rest) <- Q.minViewWithKey queue
464 ((nextScore, next), rest) <- Q.minViewWithKey queue
456− Just $ if isFinal next
465+ Just $ if isFinal next
457 then Right nextScore
466 then Right nextScore
458 else let additions = if scoreCriterion nextScore
467 else let additions = if scoreCriterion nextScore
459 then Q.fromList [ (score state, state) | state <- nextSteps next ]
468 then Q.fromList [ (score state, state) | state <- nextSteps next ]
@@ -469,19 +478,19 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
469 nextSteps :: State -> [State]
478 nextSteps :: State -> [State]
470
479
471 -- Stage 3 - match typeclasses
480 -- Stage 3 - match typeclasses
472− nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =
481+ nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =
473 if null results3 then results4 else results3
482 if null results3 then results4 else results3
474 where
483 where
475 -- try to match a typeclass argument from the left with a typeclass argument from the right
484 -- try to match a typeclass argument from the left with a typeclass argument from the right
476 results3 =
485 results3 =
477− catMaybes [ unifyQueue (State []
486+ catMaybes [ unifyQueue (State []
478 (Sided ([], deleteFromArgList n1 c1)
487 (Sided ([], deleteFromArgList n1 c1)
479 ([], map (second subst2for1) (deleteFromArgList n2 c2)))
488 ([], map (second subst2for1) (deleteFromArgList n2 c2)))
480− scoreAcc usedns) [(ty1, ty2)]
489+ scoreAcc usedns) [(ty1, ty2)]
481 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
490 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
482
491
483 -- try to hunt match a typeclass constraint by replacing it with an instance
492 -- 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)
485 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))
494 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))
486 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))
495 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))
487 | sds <- allMods ]
496 | sds <- allMods ]
@@ -512,10 +521,10 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
512 canBeFirst = map fst . filter (S.null . snd . snd)
521 canBeFirst = map fst . filter (S.null . snd . snd)
513
522
514 -- try to match an argument from the left with an argument from the right
523 -- 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)
524+ results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) hs)
516− (Sided (deleteFromDag n1 dagL, c1)
525+ (Sided (deleteFromDag n1 dagL, c1)
517 (inArgTys subst2for1 $ deleteFromDag n2 dagR, map (second subst2for1) c2))
526 (inArgTys subst2for1 $ deleteFromDag n2 dagR, map (second subst2for1) c2))
518− scoreAcc usedns) [(ty1, ty2)]
527+ scoreAcc usedns) [(ty1, ty2)]
519 | (n1, ty1) <- canBeFirst dagL, (n2, ty2) <- canBeFirst dagR
528 | (n1, ty1) <- canBeFirst dagL, (n2, ty2) <- canBeFirst dagR
520 , let subst2for1 = psubst n2 (P Bound n1 ty1)]
529 , let subst2for1 = psubst n2 (P Bound n1 ty1)]
521
530
@@ -523,7 +532,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
523
532
524 -- Stage 2 - simply introduce a subset of the typeclasses
533 -- Stage 2 - simply introduce a subset of the typeclasses
525 -- we've finished, so take some classes
534 -- we've finished, so take some classes
526− takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
535+ takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
527 map statesFromMods . prod $ both (classMods . snd) unresolved
536 map statesFromMods . prod $ both (classMods . snd) unresolved
528 where
537 where
529 swap (Sided l r) = Sided r l
538 swap (Sided l r) = Sided r l
@@ -532,7 +541,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
532 mods = swap (both snd sides) in
541 mods = swap (both snd sides) in
533 State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
542 State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
534 classMods :: Classes -> [(Classes, AsymMods)]
543 classMods :: Classes -> [(Classes, AsymMods)]
535− classMods cs = let lcs = length cs in
544+ classMods cs = let lcs = length cs in
536 [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]
545 [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]
537 prod :: Sided [a] -> [Sided a]
546 prod :: Sided [a] -> [Sided a]
538 prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]
547 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+-}
1module Idris.Unlit(unlit) where
8module Idris.Unlit(unlit) where
2
9
3import Idris.Core.TT
10import 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+-}
1module Idris.WhoCalls (whoCalls, callsWho) where
8module Idris.WhoCalls (whoCalls, callsWho) where
2
9
3import Idris.AbsSyntax
10import Idris.AbsSyntax
@@ -77,7 +84,7 @@ findOccurs :: Name -> Idris [Name]
77findOccurs n = do ctxt <- getContext
84findOccurs n = do ctxt <- getContext
78 -- A definition calls a function if the function is in the type or RHS of the definition
85 -- A definition calls a function if the function is in the type or RHS of the definition
79 let defs = (map fst . filter (\(n', def) -> n /= n' && occursDef n def) . ctxtAlist) ctxt
86 let defs = (map fst . filter (\(n', def) -> n /= n' && occursDef n def) . ctxtAlist) ctxt
80− -- A datatype calls its
87+ -- A datatype calls its
81 return defs
88 return defs
82
89
83whoCalls :: Name -> Idris [(Name, [Name])]
90whoCalls :: 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+-}
1{-# LANGUAGE CPP, ConstraintKinds #-}
8{-# LANGUAGE CPP, ConstraintKinds #-}
2#if !(MIN_VERSION_base(4,8,0))
9#if !(MIN_VERSION_base(4,8,0))
3{-# LANGUAGE OverlappingInstances #-}
10{-# 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+-}
1{-# LANGUAGE CPP #-}
8{-# LANGUAGE CPP #-}
2module Pkg.Package where
9module Pkg.Package where
3
10
src/Util/DynamicLinker.hs+12−5
@@ -1,7 +1,16 @@
1+{-|
2+Module : Util.DynamicLinker
1−-- | Platform-specific dynamic linking support. Add new platforms to this file
3+Description : Platform-specific dynamic linking support. Add new platforms to this file through conditional compilation.
2−-- through conditional compilation.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
3{-# LANGUAGE ExistentialQuantification, CPP #-}
8{-# 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
5
14
6#ifdef IDRIS_FFI
15#ifdef IDRIS_FFI
7import Foreign.LibFFI
16import Foreign.LibFFI
@@ -110,5 +119,3 @@ tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)
110tryLoadFn fn lib = do putStrLn $ "WARNING: Cannot load '" ++ fn ++ "' at compile time because Idris was compiled without libffi support."
119tryLoadFn fn lib = do putStrLn $ "WARNING: Cannot load '" ++ fn ++ "' at compile time because Idris was compiled without libffi support."
111 return Nothing
120 return Nothing
112#endif
121#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+-}
1module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where
8module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where
2
9
3import Network hiding (socketPort)
10import 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+-}
1module Util.Pretty (
8module Util.Pretty (
2− module Text.PrettyPrint.Annotated.Leijen,
9+ module Text.PrettyPrint.Annotated.Leijen
10+ , Sized(..)
3− Sized(..), nestingSize,
11+ , nestingSize
4− Pretty(..)
12+ , Pretty(..)
5−) where
13+ ) where
6
14
7--import Text.PrettyPrint.HughesPJ
15--import Text.PrettyPrint.HughesPJ
8import Text.PrettyPrint.Annotated.Leijen
16import Text.PrettyPrint.Annotated.Leijen
@@ -22,5 +30,3 @@ nestingSize = 1
22
30
23class Pretty a ty where
31class Pretty a ty where
24 pretty :: a -> Doc ty
32 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+-}
1module Util.ScreenSize(getScreenWidth) where
8module Util.ScreenSize(getScreenWidth) where
2
9
3import System.Console.Terminal.Size (size, width)
10import 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+-}
1{-# LANGUAGE CPP, ForeignFunctionInterface #-}
8{-# LANGUAGE CPP, ForeignFunctionInterface #-}
2−module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,
9+module Util.System( tempfile
10+ , withTempdir
11+ , rmFile
12+ , catchIO
13+ , isWindows
14+ , writeSource
3− writeSource, writeSourceText, readSource,
15+ , writeSourceText
16+ , readSource
4− setupBundledCC, isATTY) where
17+ , setupBundledCC
5−-- System helper functions.
18+ , isATTY
19+ ) where
6
20
7import Control.Exception as CE
21import Control.Exception as CE
8import Control.Monad (when)
22import Control.Monad (when)