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

git.iko.soy/Idris-dev

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

commit1726bf9cf16e6ea97e7e472b2dd5eeb7d1520b4d authorAhmad Salim Al-Sibahi <asal@itu.dk> dateWed 6 Apr 2016, 19:37 (11 years ago) parent6f6b894

6 files changed+33−45

compare with master

unifiedsplit

docs/reference/elaborator-reflection.rst+2−2 docs/reference/repl.rst+2−2 man/idris.1+7−19 src/Idris/CmdOptions.hs+13−13 src/Idris/Elab/Instance.hs+1−1 src/Idris/ProofSearch.hs+8−8

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

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

171171

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

173173Just 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.

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

176176

177177Using Idris's Features

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

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

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

182182Additional 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.

184184

185185

186186Recursive Elaboration

docs/reference/repl.rst+2−2

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

245245::

246246

247247 Idris> :doc Monad

248− Type class Monad

248+ Interface Monad

249249

250250 Parameters:

251251 m

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

302302::

303303

304304 Idris> :doc Monad

305− Type class Prelude.Monad.Monad

305+ Interface Prelude.Monad.Monad

306306 Methods:

307307

308308 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

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

1414

1515+ Full dependent types with dependent pattern matching

16−

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

18−

19−+ pattern matching let and lambda bindings

20−

21−+ Type classes, monad comprehensions

22−

23−+ do notation, idiom brackets

24−

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

26−

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

17++ Pattern matching let- and lambda-bindings

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

19++ do-notation, idiom brackets

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

2721+ Totality checking

28−

2922+ Coinductive types

30−

31−+ Indentation significant syntax, extensible syntax

32−

23++ Indentation significant syntax, Extensible syntax

3324+ Tactic based theorem proving (influenced by Coq)

34−

3525+ Cumulative universes

36−

37−+ Simple foreign function interface (to C)

38−

26++ Simple Foreign Function Interface

3927+ Hugs style interactive environment

4028

4129It 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

3737 PP.text "and ML.",

3838 PP.empty,

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

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

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

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

43− "+ Type classes, monad comprehensions",

44− "+ do notation, idiom brackets",

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

46− "+ Totality checking",

47− "+ Coinductive types",

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

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

50− "+ Cumulative universes",

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

52− "+ Hugs style interactive environment"

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

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

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

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

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

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

46+ "+ Totality checking",

47+ "+ Coinductive types",

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

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

50+ "+ Cumulative universes",

51+ "+ Simple Foreign Function Interface",

52+ "+ Hugs style interactive environment"

5353 ]]

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

5555 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

6767 ist <- getIState

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

6969 [c] -> return c

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

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

7171 cs -> tclift $ tfail $ At fc

7272 (CantResolveAlts (map fst cs))

7373 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

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

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

307307

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

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

309309 tryCon d locs tys n =

310310 do ty <- goal

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

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

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

337337 _ -> []

338338

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

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

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

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

341341resolveTC :: Bool -- ^ using default Int

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

343343 -> Int -- ^ depth

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

349349 = do hs <- get_holes

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

351351

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"

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

354354resTC' tcs defaultOn topholes depth topg fn elab ist

355355 = do compute

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

465465 solven n = replicateM_ n solve

466466

467467 resolve n depth

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

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

469469 | otherwise

470470 = do lams <- introImps

471471 t <- goal

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

483483 solven lams -- close any implicit lambdas we introduced

484484 ps' <- get_probs

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

486− fail "Can't apply type class"

486+ fail "Can't apply interface"

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

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

489489 t' <- goal

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

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

502502 isImp arg = (False, priority arg)

503503

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

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

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

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

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

507507findInstances ist t

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