1726bf9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed type classes in error messages and documentation to interfaces where necessary (previously forgotten)

1726bf9Ahmad Salim Al-Sibahi11 years ago

docs/reference/elaborator-reflection.rst+2−2

compare with master

unifiedsplit

@@ -171,7 +171,7 @@ Changing the Global Context

171

172``Elab`` scripts can modify the global context during execution.

173Just as the Idris elaborator produces auxiliary definitions to implement features such as ``where``-blocks and ``case`` expressions, user elaboration scripts may need to define functions.

174−Furthermore, this allows ``Elab`` reflection to be used to implement features such as type class deriving.

174+Furthermore, this allows ``Elab`` reflection to be used to implement features such as interface deriving.

175The operations ``declareType``, ``defineFunction``, and ``addInstance`` allow ``Elab`` scripts to modify the global context.

176

177Using Idris's Features

@@ -180,7 +180,7 @@ Using Idris's Features

180The Idris compiler has a number of ways to automate the construction of terms.

181On its own, the ``Elab`` state and its interactions with the unifier allow implicits to be solved using unification.

182Additional operations use further features of Idris.

183−In particular, ``resolveTC`` solves the current goal using type class resolution, ``search`` invokes the proof search mechanism, and ``sourceLocation`` finds the context in the original file at which the elaboration script is invoked.

183+In particular, ``resolveTC`` solves the current goal using interface resolution, ``search`` invokes the proof search mechanism, and ``sourceLocation`` finds the context in the original file at which the elaboration script is invoked.

184

185

186Recursive Elaboration

docs/reference/repl.rst+2−2

@@ -245,7 +245,7 @@ You can also ask for basic information about typeclasses with ``:doc``:

245::

246

247 Idris> :doc Monad

248− Type class Monad

248+ Interface Monad

249

250 Parameters:

251 m

@@ -302,7 +302,7 @@ Other documentation is also available from ``:doc``:

302::

303

304 Idris> :doc Monad

305− Type class Prelude.Monad.Monad

305+ Interface Prelude.Monad.Monad

306 Methods:

307

308 Prelude.Monad.>>= : (m : Type -> Type) -> (a : Type) -> (b : Type) -> (Monad m) -> (m a) -> (a -> m b) -> m b

man/idris.1+7−19

@@ -13,29 +13,17 @@ specified precisely in the type. It is compiled, with eager

13evaluation. Its features are influenced by Haskell and ML.

15+ Full dependent types with dependent pattern matching

16−

17−+ where clauses, with rule, simple case expressions

16++ Simple case expressions, where-clauses, with-rule

18−

19−+ pattern matching let and lambda bindings

17++ Pattern matching let- and lambda-bindings

20−

21−+ Type classes, monad comprehensions

18++ Overloading via Interfaces (Type class-like), Monad comprehensions

22−

23−+ do notation, idiom brackets

19++ do-notation, idiom brackets

24−

25−+ syntactic conveniences for lists, tuples, dependent pairs

20++ Syntactic conveniences for lists, tuples, dependent pairs

26−

27+ Totality checking

21+ Totality checking

28−

29+ Coinductive types

22+ Coinductive types

30−

31−+ Indentation significant syntax, extensible syntax

23++ Indentation significant syntax, Extensible syntax

32−

33+ Tactic based theorem proving (influenced by Coq)

24+ Tactic based theorem proving (influenced by Coq)

34−

35+ Cumulative universes

25+ Cumulative universes

36−

26++ Simple Foreign Function Interface

37−+ Simple foreign function interface (to C)

38−

39+ Hugs style interactive environment

27+ Hugs style interactive environment

41It is important to note that Idris is first and foremost a research tool

29It is important to note that Idris is first and foremost a research tool

src/Idris/CmdOptions.hs+13−13

@@ -37,19 +37,19 @@ runArgParser = do opts <- execParser $ info parser

37 PP.text "and ML.",

38 PP.empty,

39 PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [

40− "+ Full dependent types with dependent pattern matching",

40+ "+ Full dependent types with dependent pattern matching",

41− "+ where clauses, with rule, simple case expressions",

41+ "+ Simple case expressions, where-clauses, with-rule",

42− "+ pattern matching let and lambda bindings",

42+ "+ Pattern matching let- and lambda-bindings",

43− "+ Type classes, monad comprehensions",

43+ "+ Overloading via Interfaces (Type class-like), Monad comprehensions",

44− "+ do notation, idiom brackets",

44+ "+ do-notation, idiom brackets",

45− "+ syntactic conveniences for lists, tuples, dependent pairs",

45+ "+ Syntactic conveniences for lists, tuples, dependent pairs",

46− "+ Totality checking",

46+ "+ Totality checking",

47− "+ Coinductive types",

47+ "+ Coinductive types",

48− "+ Indentation significant syntax, extensible syntax",

48+ "+ Indentation significant syntax, Extensible syntax",

49− "+ Tactic based theorem proving (influenced by Coq)",

49+ "+ Tactic based theorem proving (influenced by Coq)",

50− "+ Cumulative universes",

50+ "+ Cumulative universes",

51− "+ Simple foreign function interface (to C)",

51+ "+ Simple Foreign Function Interface",

52− "+ Hugs style interactive environment"

52+ "+ Hugs style interactive environment"

53 ]]

54 idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",

55 PP.text "and project. Thus the tooling provided and resulting programs created",

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

@@ -67,7 +67,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

67 ist <- getIState

68 (n, ci) <- case lookupCtxtName n (idris_classes ist) of

69 [c] -> return c

70− [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

70+ [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

71 cs -> tclift $ tfail $ At fc

72 (CantResolveAlts (map fst cs))

73 let constraint = PApp fc (PRef fc [] n) (map pexp ps)

src/Idris/ProofSearch.hs+8−8

@@ -305,7 +305,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

305 = simple_app False (tryLocalArg d locs tys n (i - 1))

306 (psRec True d locs tys) "proof search local apply"

307

308− -- Like type class resolution, but searching with constructors

308+ -- Like interface resolution, but searching with constructors

309 tryCon d locs tys n =

310 do ty <- goal

311 let imps = case lookupCtxtExact n (idris_implicits ist) of

@@ -336,8 +336,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

336 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]

337 _ -> []

338

339−-- | Resolve type classes. This will only pick up 'normal' instances, never

339+-- | Resolve interfaces. This will only pick up 'normal' implementations, never

340−-- named instances (which is enforced by 'findInstances').

340+-- named implementations (which is enforced by 'findInstances').

341resolveTC :: Bool -- ^ using default Int

342 -> Bool -- ^ allow metavariables in the goal

343 -> Int -- ^ depth

@@ -349,7 +349,7 @@ resolveTC def mvok depth top fn elab ist

349 = do hs <- get_holes

350 resTC' [] def hs depth top fn elab ist

351

352−resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve type class"

352+resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve interface"

353resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True

354resTC' tcs defaultOn topholes depth topg fn elab ist

355 = do compute

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

465 solven n = replicateM_ n solve

466

467 resolve n depth

468− | depth == 0 = fail $ "Can't resolve type class"

468+ | depth == 0 = fail $ "Can't resolve interface"

469 | otherwise

470 = do lams <- introImps

471 t <- goal

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

483 solven lams -- close any implicit lambdas we introduced

484 ps' <- get_probs

485 when (length ps < length ps' || unrecoverable ps') $

486− fail "Can't apply type class"

486+ fail "Can't apply interface"

487-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

488 mapM_ (\ (_,n) -> do focus n

489 t' <- goal

@@ -501,8 +501,8 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

501 where isImp (PImp p _ _ _ _) = (True, p)

502 isImp arg = (False, priority arg)

503

504−-- | Find the names of instances that have been designeated for

504+-- | Find the names of implementations that have been designeated for

505−-- searching (i.e. non-named instances or instances from Elab scripts)

505+-- searching (i.e. non-named implementations or implementations from Elab scripts)

506findInstances :: IState -> Term -> [Name]

507findInstances ist t

508 | (P _ n _, _) <- unApply (getRetTy t)