ef10474 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow mutually defined instances

ef10474Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+3−2

compare with master

unifiedsplit

@@ -19,6 +19,7 @@ import System.Console.Haskeline

19import System.IO

21import Control.Monad.State

22+import Control.Monad.Error(throwError)

23import Data.List

24import Data.List

24import Data.Char

25import Data.Char

@@ -329,8 +330,8 @@ checkUndefined :: FC -> Name -> Idris ()

329checkUndefined fc n

330checkUndefined fc n

330 = do i <- getContext

331 = do i <- getContext

331 case lookupTy n i of

332 case lookupTy n i of

332− (_:_) -> fail $ show fc ++ ":" ++

333+ (_:_) -> throwError . Msg $ show fc ++ ":" ++

333− show n ++ " already defined"

334+ show n ++ " already defined"

334 _ -> return ()

335 _ -> return ()

335

336

336isUndefined :: FC -> Name -> Idris Bool

337isUndefined :: FC -> Name -> Idris Bool

src/Idris/ElabDecls.hs+11−9

@@ -1770,19 +1770,21 @@ elabClass info syn doc fc constraints tn ps ds

1770 toExp ns e sc = sc

1771

1772elabInstance :: ElabInfo -> SyntaxInfo ->

1773+ ElabWhat -> -- phase

1773 FC -> [PTerm] -> -- constraints

1774 FC -> [PTerm] -> -- constraints

1774 Name -> -- the class

1775 Name -> -- the class

1775 [PTerm] -> -- class parameters (i.e. instance)

1776 [PTerm] -> -- class parameters (i.e. instance)

1776 PTerm -> -- full instance type

1777 PTerm -> -- full instance type

1777 Maybe Name -> -- explicit name

1778 Maybe Name -> -- explicit name

1778 [PDecl] -> Idris ()

1779 [PDecl] -> Idris ()

1779−elabInstance info syn fc cs n ps t expn ds

1780+elabInstance info syn what fc cs n ps t expn ds = do

1780− = do i <- getIState

1781+ i <- getIState

1781− (n, ci) <- case lookupCtxtName n (idris_classes i) of

1782+ (n, ci) <- case lookupCtxtName n (idris_classes i) of

1782− [c] -> return c

1783+ [c] -> return c

1783− _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

1784+ _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

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

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

1785− let iname = mkiname n ps expn

1786+ let iname = mkiname n ps expn

1787+ when (what /= EDefns) $ do

1786 nty <- elabType' True info syn "" fc [] iname t

1788 nty <- elabType' True info syn "" fc [] iname t

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

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

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

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

@@ -1791,6 +1793,7 @@ elabInstance info syn fc cs n ps t expn ds

1791 (class_instances ci)

1793 (class_instances ci)

1792 addInstance intInst n iname

1794 addInstance intInst n iname

1793 Just _ -> addInstance intInst n iname

1795 Just _ -> addInstance intInst n iname

1796+ when (what /= ETypes) $ do

1794 let ips = zip (class_params ci) ps

1797 let ips = zip (class_params ci) ps

1795 let ns = case n of

1798 let ns = case n of

1796 NS n ns' -> ns'

1799 NS n ns' -> ns'

@@ -2087,9 +2090,8 @@ elabDecl' what info (PClass doc s f cs n ps ds)

2087 = do iLOG $ "Elaborating class " ++ show n

2090 = do iLOG $ "Elaborating class " ++ show n

2088 elabClass info (s { syn_params = [] }) doc f cs n ps ds

2091 elabClass info (s { syn_params = [] }) doc f cs n ps ds

2089elabDecl' what info (PInstance s f cs n ps t expn ds)

2092elabDecl' what info (PInstance s f cs n ps t expn ds)

2090− | what /= ETypes

2091 = do iLOG $ "Elaborating instance " ++ show n

2093 = do iLOG $ "Elaborating instance " ++ show n

2092− elabInstance info s f cs n ps t expn ds

2094+ elabInstance info s what f cs n ps t expn ds

2093elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

2095elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

2094 | what /= ETypes

2096 | what /= ETypes

2095 = do iLOG $ "Elaborating record " ++ show tyn

2097 = do iLOG $ "Elaborating record " ++ show tyn