f8e6549 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

:addclause now adds template bodies to instances

commitf8e6549ca9b277cb66f53a95be14befe82932134 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 12 May 2014, 01:19 (12 years ago) parentdb88c3e

3 files changed+27−8

compare with master

unifiedsplit

src/Idris/CaseSplit.hs+24−6 src/Idris/ElabDecls.hs+2−2 src/Idris/Interactive.hs+1

src/Idris/CaseSplit.hs+24−6

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

322322 -> Name -- ^ Function name

323323 -> FilePath -- ^ Source file name

324324 -> Idris String

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

326− ist <- get

327− let ap = mkApp ist ty []

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

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

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

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

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

330+ ist <- get

331+ let ap = mkApp ist ty []

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

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

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

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

331336 = let n = getNameFrom i used ty in

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

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

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

349354 ns -> uniqueNameFrom (mkSupply ns) used

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

351356

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+

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

353371 -> Name -- ^ Function name

354372 -> 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

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

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

20432043 let iname = mkiname n ps expn

2044− when (what /= EDefns) $ do

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

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

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

20472047 -- 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

20502050 (class_instances ci)

20512051 addInstance intInst n iname

20522052 Just _ -> addInstance intInst n iname

2053− when (what /= ETypes) $ do

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

20542054 let ips = zip (class_params ci) ps

20552055 let ns = case n of

20562056 NS n ns' -> ns'

src/Idris/Interactive.hs+1

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

5656 else ihPrintResult h cl

5757 where

5858 getIndent i n [] = 0

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

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

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

6162