971d88d · Idris-dev · git.iko.soy

main/Main.hs+5

compare with master

unifiedsplit

@@ -37,6 +37,7 @@ import Paths_idris

37-- Main program reads command line options, parses the main program, and gets

38-- on with the REPL.

39

40+main :: IO ()

40main = do opts <- runArgParser

41main = do opts <- runArgParser

41 runMain (runIdris opts)

42 runMain (runIdris opts)

42

43

@@ -71,17 +72,21 @@ runIdris opts = do

71 _ -> ifail "Too many packages"

72 _ -> ifail "Too many packages"

72 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

73 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

73

74

75+showver :: IO b

74showver = do putStrLn $ "Idris version " ++ ver

76showver = do putStrLn $ "Idris version " ++ ver

75 exitWith ExitSuccess

77 exitWith ExitSuccess

76

78

79+showLibs :: IO b

77showLibs = do libFlags <- getLibFlags

80showLibs = do libFlags <- getLibFlags

78 putStrLn libFlags

81 putStrLn libFlags

79 exitWith ExitSuccess

82 exitWith ExitSuccess

80

83

84+showLibdir :: IO b

81showLibdir = do dir <- getIdrisLibDir

85showLibdir = do dir <- getIdrisLibDir

82 putStrLn dir

86 putStrLn dir

83 exitWith ExitSuccess

87 exitWith ExitSuccess

84

88

89+showIncs :: IO b

85showIncs = do incFlags <- getIncFlags

90showIncs = do incFlags <- getIncFlags

86 putStrLn incFlags

91 putStrLn incFlags

87 exitWith ExitSuccess

92 exitWith ExitSuccess

src/Idris/CaseSplit.hs+8−1

@@ -5,10 +5,10 @@ module Idris.CaseSplit(splitOnLine, replaceSplits,

5 mkWith,

6 nameMissing,

7 getUniq, nameRoot) where

8−

9-- splitting a variable in a pattern clause

8-- splitting a variable in a pattern clause

10

9

11import Idris.AbsSyntax

10import Idris.AbsSyntax

11+import Idris.AbsSyntaxTree (Idris, IState, PTerm)

12import Idris.ElabDecls

13import Idris.ElabTerm

14import Idris.Delaborate

@@ -91,9 +91,11 @@ data MergeState = MS { namemap :: [(Name, Name)],

91 explicit :: [Name],

92 updates :: [(Name, PTerm)] }

93

94+addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()

94addUpdate n tm = do ms <- get

95addUpdate n tm = do ms <- get

95 put (ms { updates = ((n, stripNS tm) : updates ms) } )

96 put (ms { updates = ((n, stripNS tm) : updates ms) } )

96

97

98+inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name

97inventName ist ty n =

99inventName ist ty n =

98 do ms <- get

100 do ms <- get

99 let supp = case ty of

101 let supp = case ty of

@@ -115,11 +117,14 @@ inventName ist ty n =

115 put (ms { invented = (n, n') : invented ms })

117 put (ms { invented = (n, n') : invented ms })

116 return n'

118 return n'

117

119

120+mkSupply :: [Name] -> [Name]

118mkSupply ns = mkSupply' ns (map nextName ns)

121mkSupply ns = mkSupply' ns (map nextName ns)

119 where mkSupply' xs ns' = xs ++ mkSupply ns'

122 where mkSupply' xs ns' = xs ++ mkSupply ns'

120

123

124+varlist :: [Name]

121varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

125varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

122

126

127+stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm

123stripNS tm = mapPT dens tm where

128stripNS tm = mapPT dens tm where

124 dens (PRef fc n) = PRef fc (nsroot n)

129 dens (PRef fc n) = PRef fc (nsroot n)

125 dens t = t

130 dens t = t

@@ -310,6 +315,8 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

310 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"

315 , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"

311 | otherwise = tm

316 | otherwise = tm

312

317

318+

319+getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)

313getUniq nm i

320getUniq nm i

314 = do ist <- getIState

321 = do ist <- getIState

315 let n = nameRoot [] nm ++ "_" ++ show i

322 let n = nameRoot [] nm ++ "_" ++ show i

src/Idris/Core/Elaborate.hs+8

@@ -755,6 +755,14 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

755 if (s >= i) then (lift (tfail err), s)

756 else (f, i)

757

758+prunStateT

759+ :: Int

760+ -> Bool

761+ -> [a]

762+ -> Control.Monad.State.Strict.StateT

763+ (ElabState t) (TC' Err) t1

764+ -> ElabState t

765+ -> TC' Err ((t1, Int, Idris.Core.Unify.Fails), ElabState t)

758prunStateT pmax zok ps x s

766prunStateT pmax zok ps x s

759 = case runStateT x s of

767 = case runStateT x s of

760 OK (v, s'@(ES (p, _) _ _)) ->

768 OK (v, s'@(ES (p, _) _ _)) ->

src/Idris/Core/ProofState.hs+1

@@ -815,6 +815,7 @@ updateProblems ctxt ns ps inj holes usupp = up ns ps where

815 (ns', (x',y',env',err', while, um) : ps')

816

817-- attempt to solve remaining problems with match_unify

818+-- matchProblems :: Bool -> Elab' aux ()

818matchProblems all ns ctxt ps inj holes = up ns ps where

819matchProblems all ns ctxt ps inj holes = up ns ps where

819 up ns [] = (ns, [])

820 up ns [] = (ns, [])

820 up ns ((x, y, env, err, while, um) : ps)

821 up ns ((x, y, env, err, while, um) : ps)

src/Idris/Core/ProofTerm.hs+2

@@ -114,9 +114,11 @@ mkProofTerm tm = PT Top [] tm []

114getProofTerm :: ProofTerm -> Term

115getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

116

117+same :: Eq a => Maybe a -> a -> Bool

117same Nothing n = True

118same Nothing n = True

118same (Just x) n = x == n

119same (Just x) n = x == n

119

120

121+hole :: Binder b -> Bool

120hole (Hole _) = True

122hole (Hole _) = True

121hole (Guess _ _) = True

123hole (Guess _ _) = True

122hole _ = False

124hole _ = False

src/Idris/Core/TT.hs+1

@@ -1088,6 +1088,7 @@ unList tm = case unApply tm of

1088forget :: TT Name -> Raw

1089forget tm = forgetEnv [] tm

1090

1091+forgetEnv :: [Name] -> TT Name -> Raw

1091forgetEnv env (P _ n _) = Var n

1092forgetEnv env (P _ n _) = Var n

1092forgetEnv env (V i) = Var (env !! i)

1093forgetEnv env (V i) = Var (env !! i)

1093forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1094forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

src/Idris/Core/Unify.hs+6

@@ -84,6 +84,10 @@ match_unify ctxt env topx topy inj holes from =

84 -- but it scares me. However, matching is never guaranteed to give a unique

85 -- answer, merely a valid one, so perhaps we're okay.

86 -- In other words: it may vanish without warning some day :)

87+ un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->

88+ StateT UInfo

89+ TC [(Name, TT Name)]

90+

87 un names x tm@(App (P _ f (Bind fn (Pi t _) sc)) a)

91 un names x tm@(App (P _ f (Bind fn (Pi t _) sc)) a)

88 | (P (DCon _ _ _) _ _, _) <- unApply x,

92 | (P (DCon _ _ _) _ _, _) <- unApply x,

89 holeIn env f || f `elem` holes

93 holeIn env f || f `elem` holes

@@ -237,6 +241,7 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

237 doSubst (_ : env) tm

241 doSubst (_ : env) tm

238 = doSubst env tm

242 = doSubst env tm

239

243

244+hasv :: TT Name -> Bool

240hasv (V x) = True

245hasv (V x) = True

241hasv (App f a) = hasv f || hasv a

246hasv (App f a) = hasv f || hasv a

242hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

247hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

@@ -660,6 +665,7 @@ recoverable (Bind _ (Lam _) sc) f = recoverable sc f

660recoverable f (Bind _ (Lam _) sc) = recoverable f sc

665recoverable f (Bind _ (Lam _) sc) = recoverable f sc

661recoverable x y = True

666recoverable x y = True

662

667

668+errEnv :: [(a, Binder b)] -> [(a, b)]

663errEnv = map (\(x, b) -> (x, binderTy b))

669errEnv = map (\(x, b) -> (x, binderTy b))

664

670

665holeIn :: Env -> Name -> Bool

671holeIn :: Env -> Name -> Bool

src/Idris/Coverage.hs+29−20

@@ -120,26 +120,6 @@ genClauses fc n xs given

120 as' <- mkArg as

121 return (a':as')

122

123−fnub xs = fnub' [] xs

124−

125−fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)

126− | otherwise = fnub' (x : acc) xs

127−fnub' acc [] = acc

128−

129−-- quick check for constructor equality

130−quickEq :: PTerm -> PTerm -> Bool

131−quickEq (PConstant n) (PConstant n') = n == n'

132−quickEq (PRef _ n) (PRef _ n') = n == n'

133−quickEq (PApp _ t as) (PApp _ t' as')

134− | length as == length as'

135− = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))

136−quickEq Placeholder Placeholder = True

137−quickEq x y = False

138−

139−qelem x [] = False

140−qelem x (y : ys) | x `quickEq` y = True

141− | otherwise = qelem x ys

142−

143-- FIXME: Just look for which one is the deepest, then generate all

123-- FIXME: Just look for which one is the deepest, then generate all

144-- possibilities up to that depth.

124-- possibilities up to that depth.

145

125

@@ -244,6 +224,31 @@ genAll i args

244 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)

224 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)

245 _ -> error "Can't happen - genAll"

225 _ -> error "Can't happen - genAll"

246

226

227+ fnub :: [PTerm] -> [PTerm]

228+ fnub xs = fnub' [] xs

229+

230+ fnub' :: [PTerm] -> [PTerm] -> [PTerm]

231+ fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)

232+ | otherwise = fnub' (x : acc) xs

233+ fnub' acc [] = acc

234+

235+ -- quick check for constructor equality

236+ quickEq :: PTerm -> PTerm -> Bool

237+ quickEq (PConstant n) (PConstant n') = n == n'

238+ quickEq (PRef _ n) (PRef _ n') = n == n'

239+ quickEq (PApp _ t as) (PApp _ t' as')

240+ | length as == length as'

241+ = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))

242+ quickEq Placeholder Placeholder = True

243+ quickEq x y = False

244+

245+ qelem :: PTerm -> [PTerm] -> Bool

246+ qelem x [] = False

247+ qelem x (y : ys) | x `quickEq` y = True

248+ | otherwise = qelem x ys

249+

250+

251+upd :: t -> PArg' t -> PArg' t

247upd p' p = p { getTm = p' }

252upd p' p = p { getTm = p' }

248

253

249-- Check whether function and all descendants cover all cases (partial is

254-- Check whether function and all descendants cover all cases (partial is

@@ -706,8 +711,10 @@ checkMP ist i mp = if i > 0

706 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

711 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

707 | otherwise = Unchecked

712 | otherwise = Unchecked

708

713

714+allNothing :: [Maybe a] -> Bool

709allNothing xs = null (collapseNothing (zip xs [0..]))

715allNothing xs = null (collapseNothing (zip xs [0..]))

710

716

717+collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]

711collapseNothing ((Nothing, _) : xs)

718collapseNothing ((Nothing, _) : xs)

712 = filter (\ (x, _) -> case x of

719 = filter (\ (x, _) -> case x of

713 Nothing -> False

720 Nothing -> False

@@ -715,10 +722,12 @@ collapseNothing ((Nothing, _) : xs)

715collapseNothing (x : xs) = x : collapseNothing xs

722collapseNothing (x : xs) = x : collapseNothing xs

716collapseNothing [] = []

723collapseNothing [] = []

717

724

725+noPartial :: [Totality] -> Totality

718noPartial (Partial p : xs) = Partial p

726noPartial (Partial p : xs) = Partial p

719noPartial (_ : xs) = noPartial xs

727noPartial (_ : xs) = noPartial xs

720noPartial [] = Total []

728noPartial [] = Total []

721

729

730+collapse :: [Totality] -> Totality

722collapse xs = collapse' Unchecked xs

731collapse xs = collapse' Unchecked xs

723collapse' def (Total r : xs) = Total r

732collapse' def (Total r : xs) = Total r

724collapse' def (Unchecked : xs) = collapse' def xs

733collapse' def (Unchecked : xs) = collapse' def xs

src/Idris/Elab/Class.hs+6

@@ -103,11 +103,13 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

103 pibind [] x = x

104 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

105

106+ mdec :: Name -> Name

106 mdec (UN n) = SN (MethodN (UN n))

107 mdec (UN n) = SN (MethodN (UN n))

107 mdec (NS x n) = NS (mdec x) n

108 mdec (NS x n) = NS (mdec x) n

108 mdec x = x

109 mdec x = x

109

110

110 -- TODO: probably should normalise

111 -- TODO: probably should normalise

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

111 checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

113 checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

112 = do when (not $ null cs) . tclift

114 = do when (not $ null cs) . tclift

113 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

@@ -118,8 +120,11 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

118 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

120 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

119 return ()

121 return ()

120

122

123+ impbind :: [(Name, PTerm)] -> PTerm -> PTerm

121 impbind [] x = x

124 impbind [] x = x

122 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

125 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

126+

127+ conbind :: [PTerm] -> PTerm -> PTerm

123 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

128 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

124 conbind [] x = x

129 conbind [] x = x

125

130

@@ -155,6 +160,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

155 clause _ = False

160 clause _ = False

156

161

157 -- Generate a function for chasing a dictionary constraint

162 -- Generate a function for chasing a dictionary constraint

163+ cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> PTerm -> Idris [PDecl' PTerm]

158 cfun cn c syn all con

164 cfun cn c syn all con

159 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

165 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

160 -- SN (ParentN cn (show con))

166 -- SN (ParentN cn (show con))

src/Idris/PartialEval.hs+2

@@ -86,6 +86,7 @@ mkPE_TyDecl ist args ty = mkty args ty

86 mkty [] t = delab ist t

87

88-- | Checks if a given argument is a type class constraint argument

89+classConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

89classConstraint ist v

90classConstraint ist v

90 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of

91 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of

91 [_] -> True

92 [_] -> True

@@ -94,6 +95,7 @@ classConstraint ist v

94

95

95-- | Checks if the given arguments of a type class constraint are all either constants

96-- | Checks if the given arguments of a type class constraint are all either constants

96-- or references (i.e. that it doesn't contain any complex terms).

97-- or references (i.e. that it doesn't contain any complex terms).

98+concreteClass :: IState -> TT Name -> Bool

97concreteClass ist v

99concreteClass ist v

98 | not (classConstraint ist v) = False

100 | not (classConstraint ist v) = False

99 | (P _ c _, args) <- unApply v = all concrete args

101 | (P _ c _, args) <- unApply v = all concrete args

src/Idris/Providers.hs+5−2

@@ -7,15 +7,18 @@ import Idris.AbsSyntax

7import Idris.AbsSyntaxTree

8import Idris.Error

9

10−import Debug.Trace

11−

12-- | Wrap a type provider in the type of type providers

10-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

11providerTy :: FC -> PTerm -> PTerm

14providerTy fc tm

12providerTy fc tm

15 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

13 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

16

14

15+ioret :: Name

17ioret = sUN "prim_io_return"

16ioret = sUN "prim_io_return"

17+

18+ermod :: Name

18ermod = sNS (sUN "Error") ["Providers"]

19ermod = sNS (sUN "Error") ["Providers"]

20+

21+prmod :: Name

19prmod = sNS (sUN "Provide") ["Providers"]

22prmod = sNS (sUN "Provide") ["Providers"]

20

23

21data Provided a = Provide a

24data Provided a = Provide a