aae637d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commitaae637d43971d089bfc34ab532b8ba4c396aaaea authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 21 Mar 2018, 18:21 (9 years ago) parent7c9d72a 48a4f28

9 files changed+61−3

compare with master

unifiedsplit

docs/reference/elaborator-reflection.rst+1−1 docs/st/state.rst+1−1 libs/base/Data/IORef.idr+5 libs/contrib/Data/BoundedList.idr+15 libs/prelude/Language/Reflection/Elab.idr+9 src/Idris/Elab/Term.hs+8 test/meta003/Catch.idr+17 test/meta003/expected+2 test/meta003/run+3−1

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

@@ -6,7 +6,7 @@ Elaborator Reflection

77The Idris elaborator is responsible for converting high-level Idris code into the core language.

88It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.

9−For details, see Edwin Brady's 2013 paper in the Journal of Functional Programming.

9+For details, see [Edwin Brady's 2013 paper in the Journal of Functional Programming](https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf).

1010

1111Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.

1212This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.

docs/st/state.rst+1−1

@@ -456,7 +456,7 @@ implicit ``prf`` argument, which has the following type:

456456

457457.. code-block:: idris

458458

459− prf : InState lbl (State ty) res}

459+ prf : InState lbl (State ty) res

460460

461461This relies on a predicate ``InState``. A value of type ``InState x ty res``

462462means that the reference ``x`` must have type ``ty`` in the list of

libs/base/Data/IORef.idr+5

@@ -1,5 +1,6 @@

11module Data.IORef

3+||| A mutable variable in the IO monad.

34export

45data IORef a = MkIORef a

@@ -37,18 +38,22 @@ implementation HasReference FFI_JS where

3738 writeIORef' (MkIORef ref) val =

3839 foreign FFI_JS "%0.val = %1" (Ptr -> Ptr -> JS_IO ()) (believe_me ref) (believe_me val)

3940

41+||| Build a new IORef

4042export

4143newIORef : a -> IO (IORef a)

4244newIORef = newIORef'

4345

46+||| read the value of an IORef

4447export

4548readIORef : IORef a -> IO a

4649readIORef = readIORef'

4750

51+||| write the value of an IORef

4852export

4953writeIORef : IORef a -> a -> IO ()

5054writeIORef = writeIORef'

5155

56+||| mutate the contents of an IORef

5257export

5358modifyIORef : IORef a -> (a -> a) -> IO ()

5459modifyIORef = modifyIORef'

libs/contrib/Data/BoundedList.idr+15

@@ -1,6 +1,7 @@

11module Data.BoundedList

33import Data.Fin

4+import Data.Vect

56%access public export

67%default total

@@ -50,6 +51,20 @@ fromList : (xs : List a) -> BoundedList (length xs) a

5051fromList [] = []

5152fromList (x :: xs) = x :: fromList xs

5253

54+--------------------------------------------------------------------------------

55+-- Conversions to and from vector

56+--------------------------------------------------------------------------------

57+

58+||| Convert bounded list to vector.

59+toVect : (xs : BoundedList n a) -> Vect (finToNat (length xs)) a

60+toVect [] = []

61+toVect (x :: xs) = x :: toVect xs

62+

63+||| Convert vector to bounded list.

64+fromVect : (xs : Vect n a) -> BoundedList n a

65+fromVect [] = []

66+fromVect (x :: xs) = x :: fromVect xs

67+

5368--------------------------------------------------------------------------------

5469-- Building (bigger) bounded lists

5570--------------------------------------------------------------------------------

libs/prelude/Language/Reflection/Elab.idr+9

@@ -16,6 +16,7 @@ import Prelude.Maybe

1616import Prelude.Monad

1717import Prelude.Nat

1818import Language.Reflection

19+import Language.Reflection.Errors

1920

2021%access public export

2122

@@ -138,6 +139,7 @@ data Elab : Type -> Type where

138139 Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b

139140

140141 Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a

142+ Prim__TryCatch : {a : Type} -> Elab a -> (Err -> Elab a) -> Elab a

141143 Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a

142144

143145 Prim__Env : Elab (List (TTName, Binder TT))

@@ -218,6 +220,13 @@ namespace Tactics

218220 implementation Monad Elab where

219221 x >>= f = Prim__BindElab x f

220222

223+ ||| `tryCatch t (\err => t')` will run `t`, and if it

224+ ||| fails, roll back the elaboration state and run `t'`,

225+ ||| but with access to the knowledge of why `t` failed.

226+ export

227+ tryCatch : Elab a -> (Err -> Elab a) -> Elab a

228+ tryCatch x f = Prim__TryCatch x f

229+

221230 ||| Halt elaboration with an error

222231 export

223232 fail : List ErrorReportPart -> Elab a

src/Idris/Elab/Term.hs+8

@@ -2026,6 +2026,14 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

20262026 first' <- eval first

20272027 alt' <- eval alt

20282028 try' (runTacTm first') (runTacTm alt') True

2029+ | n == tacN "Prim__TryCatch"

2030+ = do ~[_a, first, f] <- tacTmArgs 3 tac args

2031+ first' <- eval first

2032+ f' <- eval f

2033+ tryCatch (runTacTm first') $ \err ->

2034+ do (err', _) <- checkClosed (reflectErr err)

2035+ f' <- eval (App Complete f err')

2036+ runTacTm f'

20292037 | n == tacN "Prim__Fill"

20302038 = do ~[raw] <- tacTmArgs 1 tac args

20312039 raw' <- reifyRaw =<< eval raw

test/meta003/Catch.idrnew file+17

@@ -0,0 +1,17 @@

1+import Language.Reflection.Elab

3+%language ElabReflection

5+f : Err -> Elab ()

6+f (Msg _) = fill `("message error")

7+f (CantUnify _ _ _ _ _ _) = fill `("unification error")

8+f _ = fill `("other")

10+s1 : String

11+s1 = %runElab (do tryCatch (fail []) f ; solve)

12+

13+s2 : String

14+s2 = %runElab (do tryCatch (fill `(True)) f ; solve)

15+

16+main : IO ()

17+main = do putStrLn s1 ; putStrLn s2

test/meta003/expected+2

@@ -8,3 +8,5 @@ Type mismatch between

88and

99 String

1010

11+message error

12+unification error

test/meta003/run+3−1

@@ -1,3 +1,5 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ --nocolour --check --consolewidth 70 BadDef.idr

3−rm -f *.ibc

3+${IDRIS:-idris} $@ --nocolour --consolewidth 70 -o meta003 Catch.idr

4+./meta003

5+rm -f meta003 *.ibc