3e3b098 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Give names for clauses generated with :addmissing

Names generated using the same machinery/heuristics as ordinary case split generation.

commit3e3b09836b79278b7f0500c71229fbec9781d45f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 2 Dec 2013, 16:55 (13 years ago) parent361bc6f

3 files changed+26−3

compare with master

unifiedsplit

src/Idris/CaseSplit.hs+22−1 src/Idris/ElabDecls.hs+2−1 src/Idris/REPL.hs+2−1

src/Idris/CaseSplit.hs+22−1

@@ -3,6 +3,7 @@

33module Idris.CaseSplit(splitOnLine, replaceSplits,

44 getClause, getProofClause,

55 mkWith,

6+ nameMissing,

67 getUniq, nameRoot) where

89-- splitting a variable in a pattern clause

@@ -117,7 +118,7 @@ mergeAllPats ist cv t (p : ps)

117118 = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)

118119 (MS [] [] (filter (/=cv) (patvars t)) [])

119120 ps' = mergeAllPats ist cv t ps in

120− ((p, u) : ps')

121+ ((p', u) : ps')

121122 where patvars (PRef _ n) = [n]

122123 patvars (PApp _ _ as) = concatMap (patvars . getTm) as

123124 patvars (PPatvar _ n) = [n]

@@ -357,3 +358,23 @@ mkWith str n = let str' = replaceRHS str "with (_)"

357358 | not ('=' `elem` rest) = str

358359 replaceRHS (x : rest) str = x : replaceRHS rest str

359360

361+-- Replace _ with names in missing clauses

362+

363+nameMissing :: [PTerm] -> Idris [PTerm]

364+nameMissing ps = do ist <- get

365+ newPats <- mapM nm ps

366+ let newPats' = mergeAllPats ist (UN "_") (base (head ps))

367+ newPats

368+ return (map fst newPats')

369+ where

370+ base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (UN "_")))) args)

371+ base t = t

372+

373+ nm ptm = do mptm <- elabNewPat ptm

374+ case mptm of

375+ Nothing -> return ptm

376+ Just ptm' -> return ptm'

377+

378+

379+

380+

src/Idris/ElabDecls.hs+2−1

@@ -1198,7 +1198,8 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

11981198 = do let tcgen = Dictionary `elem` opts

11991199 b <- checkPossible info fc tcgen fname lhs_in

12001200 case b of

1201− True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a valid case"

1201+ True -> tclift $ tfail (At fc

1202+ (Msg $ show lhs_in ++ " is a valid case"))

12021203 False -> do ptm <- mkPatTm lhs_in

12031204 return (Left ptm)

12041205elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

src/Idris/REPL.hs+2−1

@@ -629,7 +629,8 @@ process h fn (AddMissing updatefile l n)

629629

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

631631 [] -> return ""

632− [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms

632+ [(_, tms)] -> do tms' <- nameMissing tms

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

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

634635 if updatefile

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