db07875 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge "add definition" and "add missing" commands

db07875Edwin Brady11 years ago

CHANGELOG+2

compare with master

unifiedsplit

@@ -42,6 +42,8 @@ Tool updates

42* iPKG files have a new option `pkgs` which takes a comma-separated list

43 of package names that the idris project depends on. This reduces bloat

44 in the `opts` option with multiple package declarations.

45+* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now

46+ adds missing clauses if there is already a definition.

46Miscellaneous updates

48Miscellaneous updates

47---------------------

49---------------------

src/Idris/CaseSplit.hs+13−6

@@ -337,17 +337,21 @@ nameRoot acc nm =

337

338getClause :: Int -- ^ line number that the type is declared on

339 -> Name -- ^ Function name

340+ -> Name -- ^ User given name

340 -> FilePath -- ^ Source file name

341 -> FilePath -- ^ Source file name

341 -> Idris String

342 -> Idris String

342−getClause l fn fp

343+getClause l fn un fp

343 = do i <- getIState

344 = do i <- getIState

344 case lookupCtxt fn (idris_classes i) of

345 case lookupCtxt fn (idris_classes i) of

345 [c] -> return (mkClassBodies i (class_methods c))

346 [c] -> return (mkClassBodies i (class_methods c))

346− _ -> do ty <- getInternalApp fp l

347+ _ -> do ty_in <- getInternalApp fp l

348+ let ty = case ty_in of

349+ PTyped n t -> t

350+ x -> x

347 ist <- get

351 ist <- get

348 let ap = mkApp ist ty []

352 let ap = mkApp ist ty []

349− return (show fn ++ " " ++ ap ++ "= ?"

353+ return (show un ++ " " ++ ap ++ "= ?"

350− ++ show fn ++ "_rhs")

354+ ++ show un ++ "_rhs")

351 where mkApp :: IState -> PTerm -> [Name] -> String

355 where mkApp :: IState -> PTerm -> [Name] -> String

352 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

356 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

353 = let n = getNameFrom i used ty in

357 = let n = getNameFrom i used ty in

@@ -380,7 +384,7 @@ getClause l fn fp

380 def (show (nsroot n)) ++ " "

384 def (show (nsroot n)) ++ " "

381 ++ mkApp i ty []

385 ++ mkApp i ty []

382 ++ "= ?"

386 ++ "= ?"

383− ++ show fn ++ "_rhs_" ++ show m) ns [1..])

387+ ++ show un ++ "_rhs_" ++ show m) ns [1..])

384

388

385 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"

389 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"

386 def n = n

390 def n = n

@@ -390,7 +394,10 @@ getProofClause :: Int -- ^ line number that the type is declared

390 -> FilePath -- ^ Source file name

394 -> FilePath -- ^ Source file name

391 -> Idris String

395 -> Idris String

392getProofClause l fn fp

396getProofClause l fn fp

393− = do ty <- getInternalApp fp l

397+ = do ty_in <- getInternalApp fp l

398+ let ty = case ty_in of

399+ PTyped n t -> t

400+ x -> x

394 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")

401 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")

395 where mkApp (PPi _ _ _ _ sc) = mkApp sc

402 where mkApp (PPi _ _ _ _ sc) = mkApp sc

396 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn

403 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn

src/Idris/Elab/Clause.hs+40−39

@@ -223,46 +223,47 @@ elabClauses info' fc opts n_in cs =

223 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

224 (idris_patdefs ist) })

225 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

226− case lookupTy n ctxt of

226+ case lookupTyExact n ctxt of

227+ Just ty ->

227− [ty] -> do ctxt' <- do ctxt <- getContext

228+ do ctxt' <- do ctxt <- getContext

228− tclift $

229+ tclift $

229− addCasedef n erInfo caseInfo

230+ addCasedef n erInfo caseInfo

230− tcase defaultcase

231+ tcase defaultcase

231− reflect

232+ reflect

232− (AssertTotal `elem` opts)

233+ (AssertTotal `elem` opts)

233− atys

234+ atys

234− inacc

235+ inacc

235− pats_pe

236+ pats_pe

236− pdef

237+ pdef

237− pdef -- compile time

238+ pdef -- compile time

238− pdef_inl -- inlined

239+ pdef_inl -- inlined

239− pdef' ty

240+ pdef' ty

240− ctxt

241+ ctxt

241− setContext ctxt'

242+ setContext ctxt'

242− addIBC (IBCDef n)

243+ addIBC (IBCDef n)

243− setTotality n tot

244+ setTotality n tot

244− when (not reflect && PEGenerated `notElem` opts) $

245+ when (not reflect && PEGenerated `notElem` opts) $

245− do totcheck (fc, n)

246+ do totcheck (fc, n)

246− defer_totcheck (fc, n)

247+ defer_totcheck (fc, n)

247− when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

248+ when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

248− i <- getIState

249+ i <- getIState

249− case lookupDef n (tt_ctxt i) of

250+ case lookupDef n (tt_ctxt i) of

250− (CaseOp _ _ _ _ _ cd : _) ->

251+ (CaseOp _ _ _ _ _ cd : _) ->

251− let (scargs, sc) = cases_compiletime cd

252+ let (scargs, sc) = cases_compiletime cd

252− (scargs', sc') = cases_runtime cd in

253+ (scargs', sc') = cases_runtime cd in

253− do let calls = findCalls sc' scargs'

254+ do let calls = findCalls sc' scargs'

254− let used = findUsedArgs sc' scargs'

255+ let used = findUsedArgs sc' scargs'

255− -- let scg = buildSCG i sc scargs

256+ -- let scg = buildSCG i sc scargs

256− -- add SCG later, when checking totality

257+ -- add SCG later, when checking totality

257− let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore

258+ let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore

258− logLvl 2 $ "Called names: " ++ show cg

259+ logLvl 2 $ "Called names: " ++ show cg

259− addToCG n cg

260+ addToCG n cg

260− addToCalledG n (nub (map fst calls)) -- plus names in type!

261+ addToCalledG n (nub (map fst calls)) -- plus names in type!

261− addIBC (IBCCG n)

262+ addIBC (IBCCG n)

262− _ -> return ()

263+ _ -> return ()

263− return ()

264+ return ()

264 -- addIBC (IBCTotal n tot)

265 -- addIBC (IBCTotal n tot)

265− [] -> return ()

266+ _ -> return ()

266 -- Check it's covering, if 'covering' option is used. Chase

267 -- Check it's covering, if 'covering' option is used. Chase

267 -- all called functions, and fail if any of them are also

268 -- all called functions, and fail if any of them are also

268 -- 'Partial NotCovering'

269 -- 'Partial NotCovering'

src/Idris/Elab/Type.hs+4−3

@@ -144,12 +144,13 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

144 let nty' = normalise ctxt [] nty

145 logLvl 2 $ "Rechecked to " ++ show nty'

146

147− -- Add normalised type to internals

147+ -- Add function name to internals (used for making :addclause know

148+ -- the name unambiguously)

148 i <- getIState

149 i <- getIState

149 rep <- useREPL

150 rep <- useREPL

150 when rep $ do

151 when rep $ do

151− addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

152+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty') -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

152− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

153+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

153

154

154 let (fam, _) = unApply (getRetTy nty')

155 let (fam, _) = unApply (getRetTy nty')

155 let corec = case fam of

156 let corec = case fam of

src/Idris/Interactive.hs+32−15

@@ -47,11 +47,20 @@ caseSplitAt fn updatefile l n

47 iPrintResult new

49addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

50−addClauseFrom fn updatefile l n

50+addClauseFrom fn updatefile l n = do

51+ -- if a definition already exists, add missing cases rather than

52+ -- adding a new definition.

53+ ist <- getIState

54+ cl <- getInternalApp fn l

55+ let fulln = getAppName cl

56+

57+ case lookup fulln (idris_metavars ist) of

58+ Nothing -> addMissing fn updatefile l n

59+ Just _ -> do

51− = do src <- runIO $ readSource fn

60+ src <- runIO $ readSource fn

52 let (before, tyline : later) = splitAt (l-1) (lines src)

61 let (before, tyline : later) = splitAt (l-1) (lines src)

53 let indent = getIndent 0 (show n) tyline

62 let indent = getIndent 0 (show n) tyline

54− cl <- getClause l n fn

63+ cl <- getClause l fulln n fn

55 -- add clause before first blank line in 'later'

64 -- add clause before first blank line in 'later'

56 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

65 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

57 if updatefile

66 if updatefile

@@ -62,11 +71,16 @@ addClauseFrom fn updatefile l n

62 unlines rest)

71 unlines rest)

63 runIO $ copyFile fb fn

72 runIO $ copyFile fb fn

64 else iPrintResult cl

73 else iPrintResult cl

65− where

74+ where

66− getIndent i n [] = 0

75+ getIndent i n [] = 0

67− getIndent i n xs | take 9 xs == "instance " = i

76+ getIndent i n xs | take 9 xs == "instance " = i

68− getIndent i n xs | take (length n) xs == n = i

77+ getIndent i n xs | take (length n) xs == n = i

69− getIndent i n (x : xs) = getIndent (i + 1) n xs

78+ getIndent i n (x : xs) = getIndent (i + 1) n xs

79+

80+ getAppName (PApp _ r _) = getAppName r

81+ getAppName (PRef _ _ r) = r

82+ getAppName (PTyped n _) = getAppName n

83+ getAppName _ = n

71addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

85addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

72addProofClauseFrom fn updatefile l n

86addProofClauseFrom fn updatefile l n

@@ -98,16 +112,17 @@ addMissing fn updatefile l n

98 cl <- getInternalApp fn l

112 cl <- getInternalApp fn l

99 let n' = getAppName cl

113 let n' = getAppName cl

100

114

101− extras <- case lookupCtxt n' (idris_patdefs i) of

115+ extras <- case lookupCtxtExact n' (idris_patdefs i) of

102− [] -> return ""

116+ Nothing -> return ""

103− [(_, tms)] -> do tms' <- nameMissing tms

117+ Just (_, tms) -> do tms' <- nameMissing tms

104− showNew (show n ++ "_rhs") 1 indent tms'

118+ showNew (show n ++ "_rhs") 1 indent tms'

105− other -> return "" -- happens if called on a metavar, or with no clauses

106 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

119 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

107 if updatefile

120 if updatefile

108 then do let fb = fn ++ "~"

121 then do let fb = fn ++ "~"

109 runIO $ writeSource fb (unlines (before ++ nonblank)

122 runIO $ writeSource fb (unlines (before ++ nonblank)

123+ ++ extras ++

124+ (if null extras then ""

110− ++ extras ++ unlines rest)

125+ else "\n" ++ unlines rest))

111 runIO $ copyFile fb fn

126 runIO $ copyFile fb fn

112 else iPrintResult extras

127 else iPrintResult extras

113 where showPat = show . stripNS

128 where showPat = show . stripNS

@@ -121,6 +136,7 @@ addMissing fn updatefile l n

121

136

122 getAppName (PApp _ r _) = getAppName r

137 getAppName (PApp _ r _) = getAppName r

123 getAppName (PRef _ _ r) = r

138 getAppName (PRef _ _ r) = r

139+ getAppName (PTyped n _) = getAppName n

124 getAppName _ = n

140 getAppName _ = n

125

141

126 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '

142 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '

@@ -131,7 +147,8 @@ addMissing fn updatefile l n

131 rest <- showNew nm i' ind tms

147 rest <- showNew nm i' ind tms

132 return (makeIndent ind ++

148 return (makeIndent ind ++

133 showPat tm ++ " = ?" ++ nm' ++

149 showPat tm ++ " = ?" ++ nm' ++

150+ (if null rest then "" else

134− "\n" ++ rest)

151+ "\n" ++ rest))

135 showNew nm i _ [] = return ""

152 showNew nm i _ [] = return ""

136

153

137 getIndent i n [] = 0

154 getIndent i n [] = 0

src/Idris/REPL.hs−4

@@ -1534,7 +1534,6 @@ loadInputs inputs toline -- furthest line to read in input source files

1534 ninputs

1535 inew <- getIState

1536 let tidata = idris_tyinfodata inew

1537− let patdefs = idris_patdefs inew

1538 -- If it worked, load the whole thing from all the ibcs together

1537 -- If it worked, load the whole thing from all the ibcs together

1539 case errSpan inew of

1538 case errSpan inew of

1540 Nothing ->

1539 Nothing ->

@@ -1542,9 +1541,6 @@ loadInputs inputs toline -- furthest line to read in input source files

1542 ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

1541 ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

1543 tryLoad True (mapMaybe id ibcfiles)

1542 tryLoad True (mapMaybe id ibcfiles)

1544 _ -> return ()

1543 _ -> return ()

1545− ist <- getIState

1546− putIState $! ist { idris_tyinfodata = tidata,

1547− idris_patdefs = patdefs }

1548 exports <- findExports

1544 exports <- findExports

1549

1545

1550 case opt getOutput opts of

1546 case opt getOutput opts of