289df05 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3376 from zjhmale/fix-error-message

Use interface instead of type-class.

commit289df0561f327709948d84b6f72aad2da1c4cec3 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSun 4 Sep 2016, 20:47 (10 years ago) parent4615cff 3a0ed32

11 files changed+29−30

compare with master

unifiedsplit

src/Idris/Core/TT.hs+3−3 src/Idris/Docs.hs+1−1 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Interface.hs+6−6 src/Idris/Elab/Term.hs+1−1 src/Idris/ElabDecls.hs+2−2 src/Idris/IBC.hs+9−9 src/Idris/Parser.hs+2−3 src/Idris/ProofSearch.hs+1−1 test/interactive010/expected+2−2 test/interfaces005/expected+1−1

src/Idris/Core/TT.hs+3−3

@@ -1645,14 +1645,14 @@ showEnv' env t dbg = se 10 env t where

16451645-- | Check whether a term has any hole bindings in it - impure if so

16461646pureTerm :: TT Name -> Bool

16471647pureTerm (App _ f a) = pureTerm f && pureTerm a

1648−pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

1648+pureTerm (Bind n b sc) = notInterfaceName n && pureBinder b && pureTerm sc where

16491649 pureBinder (Hole _) = False

16501650 pureBinder (Guess _ _) = False

16511651 pureBinder (Let t v) = pureTerm t && pureTerm v

16521652 pureBinder t = pureTerm (binderTy t)

16531653

1654− notClassName (MN _ c) | c == txt "__class" = False

1655− notClassName _ = True

1654+ notInterfaceName (MN _ c) | c == txt "__interface" = False

1655+ notInterfaceName _ = True

16561656

16571657pureTerm _ = True

16581658

src/Idris/Docs.hs+1−1

@@ -102,7 +102,7 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =

102102 <> showDoc ist d

103103 <> line : showArgs args ((n, False):bnd)

104104 showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Interface constraints.

105− text "Class constraint"

105+ text "Interface constraint"

106106 <+> pprintPTerm ppo bnd [] infixes ty

107107 <> showDoc ist d

108108 <> line : showArgs args ((n, True):bnd)

src/Idris/Elab/Instance.hs+1−1

@@ -378,7 +378,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

378378 checkInInterface ns meth

379379 | any (eqRoot meth) ns = return ()

380380 | otherwise = tclift $ tfail (At fc (Msg $

381− show meth ++ " not a method of class " ++ show n))

381+ show meth ++ " not a method of interface " ++ show n))

382382

383383 eqRoot x y = nsroot x == nsroot y

384384

src/Idris/Elab/Interface.hs+6−6

@@ -113,7 +113,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

113113 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]

114114 let ddecl = PDatadecl tn NoFC tty cons

115115

116− logElab 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

116+ logElab 5 $ "Interface data " ++ show (showDImp verbosePPOption ddecl)

117117

118118 -- Elaborate the data declaration

119119 elabData info (syn { no_imp = no_imp syn ++ mnames,

@@ -164,12 +164,12 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

164164 checkDefaultSuperInterfaceInstance :: PDecl -> Idris ()

165165 checkDefaultSuperInterfaceInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _)

166166 = do when (not $ null cs) . tclift

167− $ tfail (At fc (Msg "Default superclass instances can't have constraints."))

167+ $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))

168168 i <- getIState

169169 let t = PApp fc (PRef fc [] n) (map pexp ps)

170170 let isConstrained = any (== t) (map snd constraints)

171171 when (not isConstrained) . tclift

172− $ tfail (At fc (Msg "Default instances must be for a superclass constraint on the containing class."))

172+ $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))

173173 return ()

174174

175175 checkConstraintName :: [Name] -> Name -> Idris ()

@@ -207,8 +207,8 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

207207 (\ l s p -> Imp l s p Nothing True) t'))),

208208 (n, (nfc, syn, o, t) ) )

209209 tdecl allmeths (PData doc _ syn _ _ _)

210− = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")

211− tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration")

210+ = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")

211+ tdecl _ _ = ierror $ At fc (Msg "Not allowed in an interface declaration")

212212

213213 -- Create default definitions

214214 defdecl mtys c d@(PClauses fc opts n cs) =

@@ -305,7 +305,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

305305 -- are used in the type

306306 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

307307 insertConstraint c all sc

308− = let dictN = sMN 0 "__class" in

308+ = let dictN = sMN 0 "__interface" in

309309 PPi (constraint { pstatic = Static })

310310 dictN NoFC c

311311 (constrainMeths (map basename all)

src/Idris/Elab/Term.hs+1−1

@@ -396,7 +396,7 @@ elab ist info emode opts fn tm

396396 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent interfaces

397397 = do g <- goal; resolveTC False False 5 g fn elabRec ist

398398 elab' ina fc (PResolveTC fc')

399− = do c <- getNameFrom (sMN 0 "__class")

399+ = do c <- getNameFrom (sMN 0 "__interface")

400400 instanceArg c

401401 -- Elaborate the equality type first homogeneously, then

402402 -- heterogeneously as a fallback

src/Idris/ElabDecls.hs+2−2

@@ -273,10 +273,10 @@ elabDecl' what info (PNamespace n nfc ps) =

273273

274274elabDecl' what info (PInterface doc s f cs n nfc ps pdocs fds ds cn cd)

275275 | what /= EDefns

276− = do logElab 1 $ "Elaborating class " ++ show n

276+ = do logElab 1 $ "Elaborating interface " ++ show n

277277 elabInterface info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

278278elabDecl' what info (PInstance doc argDocs s f cs pnames acc fnopts n nfc ps pextra t expn ds)

279− = do logElab 1 $ "Elaborating instance " ++ show n

279+ = do logElab 1 $ "Elaborating implementation " ++ show n

280280 elabInstance info s doc argDocs what f cs pnames acc fnopts n nfc ps pextra t expn ds

281281elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

282282 = do logElab 1 $ "Elaborating record " ++ show name

src/Idris/IBC.hs+9−9

@@ -49,7 +49,7 @@ import Codec.Archive.Zip

4949import Debug.Trace

5050

5151ibcVersion :: Word16

52−ibcVersion = 148

52+ibcVersion = 149

5353

5454-- | When IBC is being loaded - we'll load different things (and omit

5555-- different structures/definitions) depending on which phase we're in.

@@ -67,9 +67,9 @@ data IBCFile = IBCFile {

6767 , ibc_implicits :: ![(Name, [PArg])]

6868 , ibc_fixes :: ![FixDecl]

6969 , ibc_statics :: ![(Name, [Bool])]

70− , ibc_classes :: ![(Name, InterfaceInfo)]

70+ , ibc_interfaces :: ![(Name, InterfaceInfo)]

7171 , ibc_records :: ![(Name, RecordInfo)]

72− , ibc_instances :: ![(Bool, Bool, Name, Name)]

72+ , ibc_implementations :: ![(Bool, Bool, Name, Name)]

7373 , ibc_dsls :: ![(Name, DSL)]

7474 , ibc_datatypes :: ![(Name, TypeInfo)]

7575 , ibc_optimise :: ![(Name, OptInfo)]

@@ -172,9 +172,9 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

172172 makeEntry "ibc_implicits" (ibc_implicits i),

173173 makeEntry "ibc_fixes" (ibc_fixes i),

174174 makeEntry "ibc_statics" (ibc_statics i),

175− makeEntry "ibc_classes" (ibc_classes i),

175+ makeEntry "ibc_interfaces" (ibc_interfaces i),

176176 makeEntry "ibc_records" (ibc_records i),

177− makeEntry "ibc_instances" (ibc_instances i),

177+ makeEntry "ibc_implementations" (ibc_implementations i),

178178 makeEntry "ibc_dsls" (ibc_dsls i),

179179 makeEntry "ibc_datatypes" (ibc_datatypes i),

180180 makeEntry "ibc_optimise" (ibc_optimise i),

@@ -270,14 +270,14 @@ ibc i (IBCStatic n) f

270270 _ -> ifail "IBC write failed"

271271ibc i (IBCInterface n) f

272272 = case lookupCtxtExact n (idris_interfaces i) of

273− Just v -> return f { ibc_classes = (n,v): ibc_classes f }

273+ Just v -> return f { ibc_interfaces = (n,v): ibc_interfaces f }

274274 _ -> ifail "IBC write failed"

275275ibc i (IBCRecord n) f

276276 = case lookupCtxtExact n (idris_records i) of

277277 Just v -> return f { ibc_records = (n,v): ibc_records f }

278278 _ -> ifail "IBC write failed"

279279ibc i (IBCInstance int res n ins) f

280− = return f { ibc_instances = (int, res, n, ins) : ibc_instances f }

280+ = return f { ibc_implementations = (int, res, n, ins) : ibc_implementations f }

281281ibc i (IBCDSL n) f

282282 = case lookupCtxtExact n (idris_dsls i) of

283283 Just v -> return f { ibc_dsls = (n,v): ibc_dsls f }

@@ -547,7 +547,7 @@ processStatics ar = do

547547

548548processInterfaces :: Archive -> Idris ()

549549processInterfaces ar = do

550− cs <- getEntry [] "ibc_classes" ar

550+ cs <- getEntry [] "ibc_interfaces" ar

551551 mapM_ (\ (n, c) -> do

552552 i <- getIState

553553 -- Don't lose instances from previous IBCs, which

@@ -566,7 +566,7 @@ processRecords ar = do

566566

567567processInstances :: Archive -> Idris ()

568568processInstances ar = do

569− cs <- getEntry [] "ibc_instances" ar

569+ cs <- getEntry [] "ibc_implementations" ar

570570 mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs

571571

572572processDSLs :: Archive -> Idris ()

src/Idris/Parser.hs+2−3

@@ -877,8 +877,7 @@ interfaceBlock syn = do reservedHL "where"

877877 <|> fnDecl syn)

878878 closeBlock

879879 return (cn, cd', concat ds)

880− <?> "class block"

881−

880+ <?> "interface block"

882881 where

883882 constructor :: IdrisParser (Name, FC)

884883 constructor = reservedHL "constructor" *> fnName

@@ -917,7 +916,7 @@ interface_ syn = do (doc, argDocs, acc)

917916 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn)

918917 accData acc n (concatMap declared ds)

919918 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]

920− <?> "type-class declaration"

919+ <?> "interface declaration"

921920 where

922921 fundeps :: IdrisParser [(Name, FC)]

923922 fundeps = do lchar '|'; sepBy name (lchar ',')

src/Idris/ProofSearch.hs+1−1

@@ -403,7 +403,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

403403 P _ n _ -> zip (repeat n) okholePos

404404 _ -> []

405405

406− traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

406+ traceWhen ulog ("Resolving interface " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

407407 try' (trivialTCs okholes elab ist)

408408 (do addDefault t tc ttypes

409409 let stk = map fst (filter snd $ elab_stack ist)

test/interactive010/expected+2−2

@@ -4,9 +4,9 @@ a is not an implicit argument of Prelude.Interfaces./

44Usage is :doc <functionname>

55Usage is :wc <functionname>

66Usage is :printdef <functionname>

7−pat {ty504} : Type toplevel.u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}

7+pat {ty504} : Type toplevel.u. pat {__interface505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__interface505}

9− : pty {ty504} : Type toplevel.u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

9+ : pty {ty504} : Type toplevel.u. pty {__interface505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

1010(input):1:1: error: expected: ":",

1111 dependent type signature,

1212 end of input

test/interfaces005/expected+1−1

@@ -2,6 +2,6 @@ interfaces005a.idr:18:3:

22Set.TreeSet.Set must be defined by a type or data constructor

33No such variable TreeSet

44interfaces005b.idr:4:11:

5−Data definitions not allowed in a class declaration

5+Data definitions not allowed in an interface declaration

66interfaces005b.idr:18:3:SetSig is not an interface

77No such variable TreeSet