db07875 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge "add definition" and "add missing" commands

If a function already exists, then adding a definition will now add the missing cases (so in general, \d in vim or corresponding commands in other editors will now add all the necessary clauses for a covering definition.)

commitdb0787555da81d6f486bf7c639ca970bed401f7d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Oct 2015, 00:00 (11 years ago) parent8996abf

6 files changed+91−67

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/CaseSplit.hs+13−6 src/Idris/Elab/Clause.hs+40−39 src/Idris/Elab/Type.hs+4−3 src/Idris/Interactive.hs+32−15 src/Idris/REPL.hs−4

CHANGELOG+2

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

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

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

4444 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.

4547

4648Miscellaneous updates

4749---------------------

src/Idris/CaseSplit.hs+13−6

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

337337

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

339339 -> Name -- ^ Function name

340+ -> Name -- ^ User given name

340341 -> FilePath -- ^ Source file name

341342 -> Idris String

342−getClause l fn fp

343+getClause l fn un fp

343344 = do i <- getIState

344345 case lookupCtxt fn (idris_classes i) of

345346 [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

347351 ist <- get

348352 let ap = mkApp ist ty []

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

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

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

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

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

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

353357 = let n = getNameFrom i used ty in

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

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

381385 ++ mkApp i ty []

382386 ++ "= ?"

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

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

384388

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

386390 def n = n

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

390394 -> FilePath -- ^ Source file name

391395 -> Idris String

392396getProofClause 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

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

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

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

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

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

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

224224 (idris_patdefs ist) })

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

226− case lookupTy n ctxt of

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

228− tclift $

229− addCasedef n erInfo caseInfo

230− tcase defaultcase

231− reflect

232− (AssertTotal `elem` opts)

233− atys

234− inacc

235− pats_pe

236− pdef

237− pdef -- compile time

238− pdef_inl -- inlined

239− pdef' ty

240− ctxt

241− setContext ctxt'

242− addIBC (IBCDef n)

243− setTotality n tot

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

245− do totcheck (fc, n)

246− defer_totcheck (fc, n)

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

248− i <- getIState

249− case lookupDef n (tt_ctxt i) of

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

251− let (scargs, sc) = cases_compiletime cd

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

253− do let calls = findCalls sc' scargs'

254− let used = findUsedArgs sc' scargs'

255− -- let scg = buildSCG i sc scargs

256− -- add SCG later, when checking totality

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

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

259− addToCG n cg

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

261− addIBC (IBCCG n)

262− _ -> return ()

263− return ()

226+ case lookupTyExact n ctxt of

227+ Just ty ->

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

229+ tclift $

230+ addCasedef n erInfo caseInfo

231+ tcase defaultcase

232+ reflect

233+ (AssertTotal `elem` opts)

234+ atys

235+ inacc

236+ pats_pe

237+ pdef

238+ pdef -- compile time

239+ pdef_inl -- inlined

240+ pdef' ty

241+ ctxt

242+ setContext ctxt'

243+ addIBC (IBCDef n)

244+ setTotality n tot

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

246+ do totcheck (fc, n)

247+ defer_totcheck (fc, n)

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

249+ i <- getIState

250+ case lookupDef n (tt_ctxt i) of

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

252+ let (scargs, sc) = cases_compiletime cd

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

254+ do let calls = findCalls sc' scargs'

255+ let used = findUsedArgs sc' scargs'

256+ -- let scg = buildSCG i sc scargs

257+ -- add SCG later, when checking totality

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

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

260+ addToCG n cg

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

262+ addIBC (IBCCG n)

263+ _ -> return ()

264+ return ()

264265 -- addIBC (IBCTotal n tot)

265− [] -> return ()

266+ _ -> return ()

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

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

268269 -- '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

144144 let nty' = normalise ctxt [] nty

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

146146

147− -- Add normalised type to internals

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

148+ -- the name unambiguously)

148149 i <- getIState

149150 rep <- useREPL

150151 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− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

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?

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

153154

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

155156 let corec = case fam of

src/Idris/Interactive.hs+32−15

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

4747 iPrintResult new

4848

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

50−addClauseFrom fn updatefile l n

51− = do src <- runIO $ readSource fn

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

60+ src <- runIO $ readSource fn

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

5362 let indent = getIndent 0 (show n) tyline

54− cl <- getClause l n fn

63+ cl <- getClause l fulln n fn

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

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

5766 if updatefile

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

6271 unlines rest)

6372 runIO $ copyFile fb fn

6473 else iPrintResult cl

65− where

66− getIndent i n [] = 0

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

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

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

74+ where

75+ getIndent i n [] = 0

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

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

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

7084

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

7286addProofClauseFrom fn updatefile l n

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

98112 cl <- getInternalApp fn l

99113 let n' = getAppName cl

100114

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

102− [] -> return ""

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

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

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

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

116+ Nothing -> return ""

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

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

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

107120 if updatefile

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

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

110− ++ extras ++ unlines rest)

123+ ++ extras ++

124+ (if null extras then ""

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

111126 runIO $ copyFile fb fn

112127 else iPrintResult extras

113128 where showPat = show . stripNS

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

121136

122137 getAppName (PApp _ r _) = getAppName r

123138 getAppName (PRef _ _ r) = r

139+ getAppName (PTyped n _) = getAppName n

124140 getAppName _ = n

125141

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

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

131147 rest <- showNew nm i' ind tms

132148 return (makeIndent ind ++

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

134− "\n" ++ rest)

150+ (if null rest then "" else

151+ "\n" ++ rest))

135152 showNew nm i _ [] = return ""

136153

137154 getIndent i n [] = 0

src/Idris/REPL.hs−4

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

15341534 ninputs

15351535 inew <- getIState

15361536 let tidata = idris_tyinfodata inew

1537− let patdefs = idris_patdefs inew

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

15391538 case errSpan inew of

15401539 Nothing ->

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

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

15431542 tryLoad True (mapMaybe id ibcfiles)

15441543 _ -> return ()

1545− ist <- getIState

1546− putIState $! ist { idris_tyinfodata = tidata,

1547− idris_patdefs = patdefs }

15481544 exports <- findExports

15491545

15501546 case opt getOutput opts of