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

git.iko.soy/Idris-dev

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

commit3e3615ad92d91a54a53b707966c439ac76f499c4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 3 May 2012, 23:06 (14 years ago) parent46338e2

4 files changed+32−20

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−1 src/Idris/ElabDecls.hs+12−7 src/Idris/IBC.hs+11−9 src/Idris/Parser.hs+7−3

src/Idris/AbsSyntax.hs+2−1

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

497497 Name -- class

498498 [t] -- parameters

499499 t -- full instance type

500+ (Maybe Name) -- explicit name

500501 [PDecl' t]

501502 | PDSL Name (DSL' t)

502503 | PSyntax FC Syntax

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

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

17201721dumpDecl (PClass _ _ cs n ps ds)

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

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

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

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

17241725dumpDecl _ = "..."

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

src/Idris/ElabDecls.hs+12−7

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

668668 Name -> -- the class

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

670670 PTerm -> -- full instance type

671+ Maybe Name -> -- explicit name

671672 [PDecl] -> Idris ()

672−elabInstance info syn fc cs n ps t ds

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

673674 = do i <- get

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

675676 [c] -> return c

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

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

678+ let iname = case expn of

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

680+ Just nm -> nm

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

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

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

681− addInstance intInst n iname

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

683+ case expn of

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

685+ addInstance intInst n iname

686+ Just _ -> addInstance intInst n iname

682687 elabType info syn fc [] iname t

683688 let ips = zip (class_params ci) ps

684689 let ns = case n of

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

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

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

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

862867 = 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

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

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

866871 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

845845 put x4

846846 put x5

847847 put x6

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

849− put x1

850− put x2

851− put x3

852− put x4

853− put x5

854− put x6

855− put x7

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

849+ put x1

850+ put x2

851+ put x3

852+ put x4

853+ put x5

854+ put x6

855+ put x7

856+ put x8

856857 PDSL x1 x2 -> do putWord8 9

857858 put x1

858859 put x2

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

906907 x5 <- get

907908 x6 <- get

908909 x7 <- get

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

910+ x8 <- get

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

910912 9 -> do x1 <- get

911913 x2 <- get

912914 return (PDSL x1 x2)

src/Idris/Parser.hs+7−3

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

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

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

298298collect (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')

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

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

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

301301collect (d : ds) = d : collect ds

302302collect [] = []

303303

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

496496pInstance :: SyntaxInfo -> IParser [PDecl]

497497pInstance syn = do reserved "instance"

498498 fc <- pfc

499+ en <- option Nothing

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

501+ let n = expandNS syn n_in

502+ return (Just n))

499503 cs <- pConstList syn

500504 cn <- pName

501505 args <- many1 (pSimpleExpr syn)

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

504508 reserved "where"; open_block

505509 ds <- many $ pFunDecl syn

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

508512

509513--------- Expressions ---------

510514