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

git.iko.soy/Idris-dev

on master help sign in

Give names for clauses generated with :addmissing

3e3b098Edwin Brady13 years ago

src/Idris/CaseSplit.hs+22−1

compare with master

unifiedsplit

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

3module Idris.CaseSplit(splitOnLine, replaceSplits,

4 getClause, getProofClause,

5 mkWith,

6+ nameMissing,

6 getUniq, nameRoot) where

7 getUniq, nameRoot) where

8-- splitting a variable in a pattern clause

9-- splitting a variable in a pattern clause

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

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

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

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

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

119 ps' = mergeAllPats ist cv t ps in

120 ps' = mergeAllPats ist cv t ps in

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

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

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

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

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

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

123 patvars (PPatvar _ n) = [n]

124 patvars (PPatvar _ n) = [n]

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

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

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

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

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

359

360

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 [])

1198 = do let tcgen = Dictionary `elem` opts

1199 b <- checkPossible info fc tcgen fname lhs_in

1200 case b of

1201+ True -> tclift $ tfail (At fc

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

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

1202 False -> do ptm <- mkPatTm lhs_in

1203 False -> do ptm <- mkPatTm lhs_in

1203 return (Left ptm)

1204 return (Left ptm)

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

1205elabClause 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)

629

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

631 [] -> return ""

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

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

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

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

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

634 if updatefile

635 if updatefile

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

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