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

git.iko.soy/Idris-dev

Annotate several top-level functions

commit971d88d592ea67beaa7a0c5e7f52cafd87e1db70 authorMichael Maloney <tactics40@gmail.com> dateMon 1 Sep 2014, 06:58 (12 years ago) parent4dc73a0

11 files changed+73−23

compare with master

unifiedsplit

main/Main.hs+5 src/Idris/CaseSplit.hs+8−1 src/Idris/Core/Elaborate.hs+8 src/Idris/Core/ProofState.hs+1 src/Idris/Core/ProofTerm.hs+2 src/Idris/Core/TT.hs+1 src/Idris/Core/Unify.hs+6 src/Idris/Coverage.hs+29−20 src/Idris/Elab/Class.hs+6 src/Idris/PartialEval.hs+2 src/Idris/Providers.hs+5−2

main/Main.hs+5

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

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

3838-- on with the REPL.

3939

40+main :: IO ()

4041main = do opts <- runArgParser

4142 runMain (runIdris opts)

4243

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

7172 _ -> ifail "Too many packages"

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

7374

75+showver :: IO b

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

7577 exitWith ExitSuccess

7678

79+showLibs :: IO b

7780showLibs = do libFlags <- getLibFlags

7881 putStrLn libFlags

7982 exitWith ExitSuccess

8083

84+showLibdir :: IO b

8185showLibdir = do dir <- getIdrisLibDir

8286 putStrLn dir

8387 exitWith ExitSuccess

8488

89+showIncs :: IO b

8590showIncs = do incFlags <- getIncFlags

8691 putStrLn incFlags

8792 exitWith ExitSuccess

src/Idris/CaseSplit.hs+8−1

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

55 mkWith,

66 nameMissing,

77 getUniq, nameRoot) where

8−

98-- splitting a variable in a pattern clause

109

1110import Idris.AbsSyntax

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

1212import Idris.ElabDecls

1313import Idris.ElabTerm

1414import Idris.Delaborate

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

9191 explicit :: [Name],

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

9393

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

9495addUpdate n tm = do ms <- get

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

9697

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

9799inventName ist ty n =

98100 do ms <- get

99101 let supp = case ty of

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

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

116118 return n'

117119

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

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

119122 where mkSupply' xs ns' = xs ++ mkSupply ns'

120123

124+varlist :: [Name]

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

122126

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

123128stripNS tm = mapPT dens tm where

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

125130 dens t = t

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

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

311316 | otherwise = tm

312317

318+

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

313320getUniq nm i

314321 = do ist <- getIState

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

src/Idris/Core/Elaborate.hs+8

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

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

756756 else (f, i)

757757

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)

758766prunStateT pmax zok ps x s

759767 = case runStateT x s of

760768 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

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

816816

817817-- attempt to solve remaining problems with match_unify

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

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

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

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

src/Idris/Core/ProofTerm.hs+2

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

114114getProofTerm :: ProofTerm -> Term

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

116116

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

117118same Nothing n = True

118119same (Just x) n = x == n

119120

121+hole :: Binder b -> Bool

120122hole (Hole _) = True

121123hole (Guess _ _) = True

122124hole _ = False

src/Idris/Core/TT.hs+1

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

10881088forget :: TT Name -> Raw

10891089forget tm = forgetEnv [] tm

10901090

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

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

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

10931094forgetEnv 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 =

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

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

8686 -- 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+

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

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

8993 holeIn env f || f `elem` holes

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

237241 doSubst (_ : env) tm

238242 = doSubst env tm

239243

244+hasv :: TT Name -> Bool

240245hasv (V x) = True

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

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

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

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

661666recoverable x y = True

662667

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

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

664670

665671holeIn :: Env -> Name -> Bool

src/Idris/Coverage.hs+29−20

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

120120 as' <- mkArg as

121121 return (a':as')

122122

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−

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

144124-- possibilities up to that depth.

145125

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

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

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

246226

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

247252upd p' p = p { getTm = p' }

248253

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

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

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

707712 | otherwise = Unchecked

708713

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

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

710716

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

711718collapseNothing ((Nothing, _) : xs)

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

713720 Nothing -> False

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

715722collapseNothing (x : xs) = x : collapseNothing xs

716723collapseNothing [] = []

717724

725+noPartial :: [Totality] -> Totality

718726noPartial (Partial p : xs) = Partial p

719727noPartial (_ : xs) = noPartial xs

720728noPartial [] = Total []

721729

730+collapse :: [Totality] -> Totality

722731collapse xs = collapse' Unchecked xs

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

724733collapse' 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

103103 pibind [] x = x

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

105105

106+ mdec :: Name -> Name

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

107108 mdec (NS x n) = NS (mdec x) n

108109 mdec x = x

109110

110111 -- TODO: probably should normalise

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

113115 $ 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

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

119121 return ()

120122

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

121124 impbind [] x = x

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

126+

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

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

124129 conbind [] x = x

125130

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

155160 clause _ = False

156161

157162 -- Generate a function for chasing a dictionary constraint

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

158164 cfun cn c syn all con

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

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

src/Idris/PartialEval.hs+2

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

8686 mkty [] t = delab ist t

8787

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

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

8990classConstraint ist v

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

9192 [_] -> True

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

9495

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

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

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

9799concreteClass ist v

98100 | not (classConstraint ist v) = False

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

src/Idris/Providers.hs+5−2

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

77import Idris.AbsSyntaxTree

88import Idris.Error

10−import Debug.Trace

11−

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

1311providerTy :: FC -> PTerm -> PTerm

1412providerTy fc tm

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

1614

15+ioret :: Name

1716ioret = sUN "prim_io_return"

17+

18+ermod :: Name

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

20+

21+prmod :: Name

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

2023

2124data Provided a = Provide a