f8e6549 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

:addclause now adds template bodies to instances

f8e6549Edwin Brady12 years ago

src/Idris/CaseSplit.hs+24−6

compare with master

unifiedsplit

@@ -322,12 +322,17 @@ getClause :: Int -- ^ line number that the type is declared on

322 -> Name -- ^ Function name

323 -> FilePath -- ^ Source file name

324 -> Idris String

325+getClause l fn fp

326+ = do i <- getIState

327+ case lookupCtxt fn (idris_classes i) of

328+ [c] -> return (mkClassBodies i (class_methods c))

325−getClause l fn fp = do ty <- getInternalApp fp l

329+ _ -> do ty <- getInternalApp fp l

326− ist <- get

330+ ist <- get

327− let ap = mkApp ist ty []

331+ let ap = mkApp ist ty []

328− return (show fn ++ " " ++ ap ++

332+ return (show fn ++ " " ++ ap ++ "= ?"

329− "= ?" ++ show fn ++ "_rhs")

333+ ++ show fn ++ "_rhs")

334+ where mkApp :: IState -> PTerm -> [Name] -> String

330− where mkApp i (PPi (Exp _ _ False) (MN _ _) ty sc) used

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

331 = let n = getNameFrom i used ty in

336 = let n = getNameFrom i used ty in

332 show n ++ " " ++ mkApp i sc (n : used)

337 show n ++ " " ++ mkApp i sc (n : used)

333 mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used

338 mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used

@@ -349,6 +354,19 @@ getClause l fn fp = do ty <- getInternalApp fp l

349 ns -> uniqueNameFrom (mkSupply ns) used

354 ns -> uniqueNameFrom (mkSupply ns) used

350 getNameFrom i used _ = uniqueName (sUN "x") used

355 getNameFrom i used _ = uniqueName (sUN "x") used

351

356

357+ -- write method declarations, indent with 4 spaces

358+ mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

359+ mkClassBodies i ns

360+ = showSep "\n"

361+ (zipWith (\(n, (_, ty)) m -> " " ++

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

363+ ++ mkApp i ty []

364+ ++ "= ?"

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

366+

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

368+ def n = n

369+

352getProofClause :: Int -- ^ line number that the type is declared

370getProofClause :: Int -- ^ line number that the type is declared

353 -> Name -- ^ Function name

371 -> Name -- ^ Function name

354 -> FilePath -- ^ Source file name

372 -> FilePath -- ^ Source file name

src/Idris/ElabDecls.hs+2−2

@@ -2041,7 +2041,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2041 (CantResolveAlts (map (show . fst) cs))

2042 let constraint = PApp fc (PRef fc n) (map pexp ps)

2043 let iname = mkiname n ps expn

2044− when (what /= EDefns) $ do

2044+ when (what /= EDefns || null ds) $ do

2045 nty <- elabType' True info syn emptyDocstring [] fc [] iname t

2046 -- if the instance type matches any of the instances we have already,

2047 -- and it's not a named instance, then it's overlapping, so report an error

@@ -2050,7 +2050,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2050 (class_instances ci)

2051 addInstance intInst n iname

2052 Just _ -> addInstance intInst n iname

2053− when (what /= ETypes) $ do

2053+ when (what /= ETypes && (not (null ds))) $ do

2054 let ips = zip (class_params ci) ps

2055 let ns = case n of

2056 NS n ns' -> ns'

src/Idris/Interactive.hs+1

@@ -56,6 +56,7 @@ addClauseFrom h fn updatefile l n

56 else ihPrintResult h cl

57 where

58 getIndent i n [] = 0

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

59 getIndent i n xs | take (length n) xs == n = i

60 getIndent i n xs | take (length n) xs == n = i

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

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