aae637d · Idris-dev · git.iko.soy

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

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

6

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

8It 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).

10

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

12This 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:

456

457.. code-block:: idris

458

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

459+ prf : InState lbl (State ty) res

460

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

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

libs/base/Data/IORef.idr+5

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

1module Data.IORef

2

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

3export

4export

4data IORef a = MkIORef a

5data IORef a = MkIORef a

5

6

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

37 writeIORef' (MkIORef ref) val =

38 writeIORef' (MkIORef ref) val =

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

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

39

40

41+||| Build a new IORef

40export

42export

41newIORef : a -> IO (IORef a)

43newIORef : a -> IO (IORef a)

42newIORef = newIORef'

44newIORef = newIORef'

43

45

46+||| read the value of an IORef

44export

47export

45readIORef : IORef a -> IO a

48readIORef : IORef a -> IO a

46readIORef = readIORef'

49readIORef = readIORef'

47

50

51+||| write the value of an IORef

48export

52export

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

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

50writeIORef = writeIORef'

54writeIORef = writeIORef'

51

55

56+||| mutate the contents of an IORef

52export

57export

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

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

54modifyIORef = modifyIORef'

59modifyIORef = modifyIORef'

libs/contrib/Data/BoundedList.idr+15

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

1module Data.BoundedList

2

3import Data.Fin

4+import Data.Vect

4

5

5%access public export

6%access public export

6%default total

7%default total

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

50fromList [] = []

51fromList [] = []

51fromList (x :: xs) = x :: fromList xs

52fromList (x :: xs) = x :: fromList xs

52

53

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+

53--------------------------------------------------------------------------------

68--------------------------------------------------------------------------------

54-- Building (bigger) bounded lists

69-- Building (bigger) bounded lists

55--------------------------------------------------------------------------------

70--------------------------------------------------------------------------------

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

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

16import Prelude.Monad

17import Prelude.Nat

18import Language.Reflection

19+import Language.Reflection.Errors

19

20

20%access public export

21%access public export

21

22

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

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

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

139

140

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

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

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

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

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

142

144

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

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

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

218 implementation Monad Elab where

220 implementation Monad Elab where

219 x >>= f = Prim__BindElab x f

221 x >>= f = Prim__BindElab x f

220

222

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+

221 ||| Halt elaboration with an error

230 ||| Halt elaboration with an error

222 export

231 export

223 fail : List ErrorReportPart -> Elab a

232 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

2026 first' <- eval first

2027 alt' <- eval alt

2028 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'

2029 | n == tacN "Prim__Fill"

2037 | n == tacN "Prim__Fill"

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

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

2031 raw' <- reifyRaw =<< eval raw

2039 raw' <- reifyRaw =<< eval raw

test/meta003/Catch.idrnew file+17

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

1+import Language.Reflection.Elab

2+

3+%language ElabReflection

4+

5+f : Err -> Elab ()

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

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

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

9+

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

8and

9 String

10

11+message error

12+unification error

test/meta003/run+3−1

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

1#!/usr/bin/env bash

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

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

4+./meta003

3−rm -f *.ibc

5+rm -f meta003 *.ibc