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

git.iko.soy/Idris-dev

on master help sign in

Allow explicit names on type class instances (for explicit resolution)

3e3615aEdwin Brady14 years ago

src/Idris/AbsSyntax.hs+2−1

compare with master

unifiedsplit

@@ -497,6 +497,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

497 Name -- class

498 [t] -- parameters

499 t -- full instance type

500+ (Maybe Name) -- explicit name

500 [PDecl' t]

501 [PDecl' t]

501 | PDSL Name (DSL' t)

502 | PDSL Name (DSL' t)

502 | PSyntax FC Syntax

503 | PSyntax FC Syntax

@@ -1719,7 +1720,7 @@ dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"

1719dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

1720dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

1720dumpDecl (PClass _ _ cs n ps ds)

1721dumpDecl (PClass _ _ cs n ps ds)

1721 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

1722 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

1722−dumpDecl (PInstance _ _ cs n _ t ds)

1723+dumpDecl (PInstance _ _ cs n _ t _ ds)

1723 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

1724 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

1724dumpDecl _ = "..."

1725dumpDecl _ = "..."

1725-- dumpDecl (PImport i) = "import " ++ i

1726-- dumpDecl (PImport i) = "import " ++ i

src/Idris/ElabDecls.hs+12−7

@@ -668,17 +668,22 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

668 Name -> -- the class

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

670 PTerm -> -- full instance type

671+ Maybe Name -> -- explicit name

671 [PDecl] -> Idris ()

672 [PDecl] -> Idris ()

672−elabInstance info syn fc cs n ps t ds

673+elabInstance info syn fc cs n ps t expn ds

673 = do i <- get

674 = do i <- get

674 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

675 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

675 [c] -> return c

676 [c] -> return c

676 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

677 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

678+ let iname = case expn of

677− let iname = UN ('@':show n ++ "$" ++ show ps)

679+ Nothing -> UN ('@':show n ++ "$" ++ show ps)

680+ Just nm -> nm

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

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

679− -- then it's overlapping, so report an error

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

683+ case expn of

680− mapM_ (checkNotOverlapping i t) (class_instances ci)

684+ Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci)

685+ addInstance intInst n iname

681− addInstance intInst n iname

686+ Just _ -> addInstance intInst n iname

682 elabType info syn fc [] iname t

687 elabType info syn fc [] iname t

683 let ips = zip (class_params ci) ps

688 let ips = zip (class_params ci) ps

684 let ns = case n of

689 let ns = case n of

@@ -858,9 +863,9 @@ elabDecl' info (PNamespace n ps) = mapM_ (elabDecl' ninfo) ps

858 Just ns -> info { namespace = Just (n:ns) }

863 Just ns -> info { namespace = Just (n:ns) }

859elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n

864elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n

860 elabClass info s f cs n ps ds

865 elabClass info s f cs n ps ds

861−elabDecl' info (PInstance s f cs n ps t ds)

866+elabDecl' info (PInstance s f cs n ps t expn ds)

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

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

863− elabInstance info s f cs n ps t ds

868+ elabInstance info s f cs n ps t expn ds

864elabDecl' info (PRecord s f tyn ty cn cty)

869elabDecl' info (PRecord s f tyn ty cn cty)

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

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

866 elabRecord info s f tyn ty cn cty

871 elabRecord info s f tyn ty cn cty

src/Idris/IBC.hs+11−9

@@ -845,14 +845,15 @@ instance (Binary t) => Binary (PDecl' t) where

845 put x4

846 put x5

847 put x6

848− PInstance x1 x2 x3 x4 x5 x6 x7 -> do putWord8 8

848+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

849− put x1

849+ put x1

850− put x2

850+ put x2

851− put x3

851+ put x3

852− put x4

852+ put x4

853− put x5

853+ put x5

854− put x6

854+ put x6

855− put x7

855+ put x7

856+ put x8

856 PDSL x1 x2 -> do putWord8 9

857 PDSL x1 x2 -> do putWord8 9

857 put x1

858 put x1

858 put x2

859 put x2

@@ -906,7 +907,8 @@ instance (Binary t) => Binary (PDecl' t) where

906 x5 <- get

907 x5 <- get

907 x6 <- get

908 x6 <- get

908 x7 <- get

909 x7 <- get

910+ x8 <- get

909− return (PInstance x1 x2 x3 x4 x5 x6 x7)

911+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

910 9 -> do x1 <- get

912 9 -> do x1 <- get

911 x2 <- get

913 x2 <- get

912 return (PDSL x1 x2)

914 return (PDSL x1 x2)

src/Idris/Parser.hs+7−3

@@ -296,8 +296,8 @@ collect (c@(PClauses _ o _ _) : ds)

296collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

297collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

298collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

299−collect (PInstance f s cs n ps t ds : ds')

299+collect (PInstance f s cs n ps t en ds : ds')

300− = PInstance f s cs n ps t (collect ds) : collect ds'

300+ = PInstance f s cs n ps t en (collect ds) : collect ds'

301collect (d : ds) = d : collect ds

302collect [] = []

303

@@ -496,6 +496,10 @@ pClass syn = do acc <- pAccessibility

496pInstance :: SyntaxInfo -> IParser [PDecl]

497pInstance syn = do reserved "instance"

498 fc <- pfc

499+ en <- option Nothing

500+ (do lchar '['; n_in <- pfName; lchar ']'

501+ let n = expandNS syn n_in

502+ return (Just n))

499 cs <- pConstList syn

503 cs <- pConstList syn

500 cn <- pName

504 cn <- pName

501 args <- many1 (pSimpleExpr syn)

505 args <- many1 (pSimpleExpr syn)

@@ -504,7 +508,7 @@ pInstance syn = do reserved "instance"

504 reserved "where"; open_block

508 reserved "where"; open_block

505 ds <- many $ pFunDecl syn

509 ds <- many $ pFunDecl syn

506 close_block

510 close_block

507− return [PInstance syn fc cs cn args t (concat ds)]

511+ return [PInstance syn fc cs cn args t en (concat ds)]

508

512

509--------- Expressions ---------

513--------- Expressions ---------

510

514