53fae80 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

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

1669pureTerm :: TT Name -> Bool

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

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

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

1672 pureBinder (Hole _) = False

1673 pureBinder (Guess _ _) = False

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

1675 pureBinder t = pureTerm (binderTy t)

1676

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

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

1678− notClassName _ = True

1678+ notInterfaceName _ = True

1679

1680pureTerm _ = True

1681

src/Idris/Docs.hs+1−1

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

102 <> showDoc ist d

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

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

105− text "Class constraint"

105+ text "Interface constraint"

106 <+> pprintPTerm ppo bnd [] infixes ty

107 <> showDoc ist d

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

378 checkInInterface ns meth

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

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

382

383 eqRoot x y = nsroot x == nsroot y

384

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

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

114 let ddecl = PDatadecl tn NoFC tty cons

115

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

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

117

118 -- Elaborate the data declaration

119 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

164 checkDefaultSuperInterfaceInstance :: PDecl -> Idris ()

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

166 = 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."))

168 i <- getIState

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

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

171 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."))

173 return ()

174

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

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

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

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

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

210− = ierror $ At fc (Msg "Data definitions 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 a class declaration")

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

212

213 -- Create default definitions

214 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

305 -- are used in the type

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

307 insertConstraint c all sc

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

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

309 PPi (constraint { pstatic = Static })

310 dictN NoFC c

311 (constrainMeths (map basename all)

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

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

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

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

398 elab' ina fc (PResolveTC fc')

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

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

400 instanceArg c

401 -- Elaborate the equality type first homogeneously, then

402 -- heterogeneously as a fallback

src/Idris/ElabDecls.hs+2−2

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

273

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

275 | what /= EDefns

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

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

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

278elabDecl' 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

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

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

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

src/Idris/IBC.hs+8−8

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

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

68 , ibc_fixes :: ![FixDecl]

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

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

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

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

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

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

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

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

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

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

172 makeEntry "ibc_implicits" (ibc_implicits i),

173 makeEntry "ibc_fixes" (ibc_fixes i),

174 makeEntry "ibc_statics" (ibc_statics i),

175− makeEntry "ibc_classes" (ibc_classes i),

175+ makeEntry "ibc_interfaces" (ibc_interfaces i),

176 makeEntry "ibc_records" (ibc_records i),

177− makeEntry "ibc_instances" (ibc_instances i),

177+ makeEntry "ibc_implementations" (ibc_implementations i),

178 makeEntry "ibc_dsls" (ibc_dsls i),

179 makeEntry "ibc_datatypes" (ibc_datatypes i),

180 makeEntry "ibc_optimise" (ibc_optimise i),

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

270 _ -> ifail "IBC write failed"

271ibc i (IBCInterface n) f

272 = 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 }

274 _ -> ifail "IBC write failed"

275ibc i (IBCRecord n) f

276 = case lookupCtxtExact n (idris_records i) of

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

278 _ -> ifail "IBC write failed"

279ibc 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 }

281ibc i (IBCDSL n) f

282 = case lookupCtxtExact n (idris_dsls i) of

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

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

547

548processInterfaces :: Archive -> Idris ()

549processInterfaces ar = do

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

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

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

552 i <- getIState

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

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

566

567processInstances :: Archive -> Idris ()

568processInstances ar = do

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

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

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

571

572processDSLs :: Archive -> Idris ()

src/Idris/Parser.hs+2−3

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

877 <|> fnDecl syn)

878 closeBlock

879 return (cn, cd', concat ds)

880− <?> "class block"

880+ <?> "interface block"

881−

882 where

881 where

883 constructor :: IdrisParser (Name, FC)

882 constructor :: IdrisParser (Name, FC)

884 constructor = reservedHL "constructor" *> fnName

883 constructor = reservedHL "constructor" *> fnName

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

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

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

918 accData acc n (concatMap declared ds)

917 accData acc n (concatMap declared ds)

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

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

920− <?> "type-class declaration"

919+ <?> "interface declaration"

921 where

920 where

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

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

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

922 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

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

404 _ -> []

405

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

407 try' (trivialTCs okholes elab ist)

408 (do addDefault t tc ttypes

409 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./

4Usage is :doc <functionname>

5Usage is :wc <functionname>

6Usage 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}

8

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}

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

11 dependent type signature,

12 end of input

test/interfaces005/expected+1−1

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

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

3No such variable TreeSet

4interfaces005b.idr:4:11:

5−Data definitions not allowed in a class declaration

5+Data definitions not allowed in an interface declaration

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

7No such variable TreeSet