git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
5a8ca14Edwin Brady
CHANGELOG.md+2
compare with master
unifiedsplit
@@ -20,6 +20,8 @@
20 correct st = record { score->correct $= (+1),
20 correct st = record { score->correct $= (+1),
21 score->attempted $= (+1) } st
21 score->attempted $= (+1) } st
22 ```
22 ```
23+* The File Effect has been updated to take into account changes in
24+ `Prelude.File` and to provide a 'better' API.
23
25
24# New in 0.12:
26# New in 0.12:
25
27
docs/tutorial/typesfuns.rst+89
@@ -685,6 +685,95 @@ without any explicit use of ``Force`` or ``Delay``:
685 ifThenElse True t e = t;
685 ifThenElse True t e = t;
686 ifThenElse False t e = e;
686 ifThenElse False t e = e;
687
687
688+Codata Types
689+============
690+
691+Codata types are like regular data types, except that they allow for us to
692+define infinite data structures. More precisely, for a type ``T``, each of its
693+constructor arguments of type ``T`` are transformed into a coinductive parameter
694+``Inf T``. This makes each of the ``T`` arguments lazy, and allows infinite data
695+structures of type ``T`` to be built. One example of a codata type is Stream,
696+which is defined as follows.
697+
698+.. code-block:: idris
699+
700+ codata Stream : Type -> Type where
701+ (::) : (e : a) -> Stream a -> Stream a
702+
703+This gets translated into the following by the compiler.
704+
705+.. code-block:: idris
706+
707+ data Stream : Type -> Type where
708+ (::) : (e : a) -> Inf (Stream a) -> Stream a
709+
710+The following is an example of how the codata type ``Stream`` can be used to
711+form an infinite data structure. In this case we are creating an infinite stream
712+of ones.
713+
714+.. code-block:: idris
715+
716+ ones :: Stream Nat
717+ ones = 1 :: ones
718+
719+It is important to note that codata does not allow the creation of infinite
720+mutually recursive data structures. For example the following will create an
721+infinite loop and cause a stack overflow.
722+
723+.. code-block:: idris
724+
725+ mutual
726+ codata Blue a = B a (Red a)
727+ codata Red a = R a (Blue a)
728+
729+ mutual
730+ blue : Blue Nat
731+ blue = B 1 red
732+
733+ red : Red Nat
734+ red = R 1 blue
735+
736+ mutual
737+ findB : (a -> Bool) -> Blue a -> a
738+ findB f (B x r) = if f x then x else findR f r
739+
740+ findR : (a -> Bool) -> Red a -> a
741+ findR f (R x b) = if f x then x else findB f b
742+
743+ main : IO ()
744+ main = do printLn $ findB (== 1) blue
745+
746+To fix this we must add explicit ``Inf`` declarations to the constructor
747+parameter types, since codata will not add it to constructor parameters of a
748+**different** type from the one being defined. For example, the following
749+outputs "1".
750+
751+.. code-block:: idris
752+
753+ mutual
754+ data Blue : Type -> Type where
755+ B : a -> Inf (Red a) -> Blue a
756+
757+ data Red : Type -> Type where
758+ R : a -> Inf (Blue a) -> Red a
759+
760+ mutual
761+ blue : Blue Nat
762+ blue = B 1 red
763+
764+ red : Red Nat
765+ red = R 1 blue
766+
767+ mutual
768+ findB : (a -> Bool) -> Blue a -> a
769+ findB f (B x r) = if f x then x else findR f r
770+
771+ findR : (a -> Bool) -> Red a -> a
772+ findR f (R x b) = if f x then x else findB f b
773+
774+ main : IO ()
775+ main = do printLn $ findB (== 1) blue
776+
688Useful Data Types
777Useful Data Types
689=================
778=================
690
779
libs/effects/Effect/File.idr+397−162
@@ -1,4 +1,4 @@
1−-- -------------------------------------------------------- [ Effectful FileIO ]
1+||| Effectful file operations.
2module Effect.File
2module Effect.File
3
3
4import Effects
4import Effects
@@ -6,188 +6,423 @@ import Control.IOExcept
6
6
7%access public export
7%access public export
8
8
9−||| A Dependent type to describe File Handles. File handles are
9+-- -------------------------------------------------------------- [ Predicates ]
10−||| parameterised with the current state of the file: Closed; Open for
11−||| reading; and Open for writing.
12−|||
13−||| @ m The file mode.
14−data OpenFile : (m : Mode) -> Type where
15− FH : File -> OpenFile m
16
10
17−openOK : Mode -> Bool -> Type
11+||| A record of the file modes that can read from a file.
18−openOK m True = OpenFile m
12+data ValidModeRead : Mode -> Type where
19−openOK m False = ()
13+ VMRRead : ValidModeRead Read
14+ VMRReadW : ValidModeRead ReadWrite
15+ VMRReadWT : ValidModeRead ReadWriteTruncate
16+ VMRReadA : ValidModeRead ReadAppend
20
17
21−-- ------------------------------------------------------------ [ The Protocol ]
18+||| A record of the file modes that can write from a file.
19+data ValidModeWrite : Mode -> Type where
20+ VMWWrite : ValidModeWrite WriteTruncate
21+ VMWAppend : ValidModeWrite Append
22+ VMWReadW : ValidModeWrite ReadWrite
23+ VMWReadWT : ValidModeWrite ReadWriteTruncate
22
24
23−||| Here the protocol for resource access is defined as an effect.
25+-- -------------------------------------------------- [ Custom Error Reporting ]
24−||| The state transitions diagram for the protocol is as follows:
26+
25−|||
27+namespace FileResult
26−||| digraph G {
28+
29+ ||| A type to describe the return type of file operations.
30+ data ResultDesc = SUCCESS | RESULT
31+
32+ ||| A custom return type for file operations that is dependent on
33+ ||| the type of file operation.
34+ |||
35+ ||| @desc Parameterises the constructors to describe if the function
36+ ||| returns a value or not.
37+ ||| @ty The return type for a file operation that returns a value.
38+ |||
39+ data FileOpReturnTy : (desc : ResultDesc)
40+ -> (ty : Type)
41+ -> Type where
42+
43+ ||| The operation completed successfully and doesn't return a
44+ ||| result.
45+ Success : FileOpReturnTy SUCCESS ty
46+
47+ ||| The operation returns a result of type `ty`.
48+ |||
49+ ||| @ty The value returned.
50+ Result : ty -> FileOpReturnTy RESULT ty
51+
52+ ||| The operation failed and the RTS produced the given error.
53+ |||
54+ ||| @err The reported error code.
55+ FError : (err : FileError) -> FileOpReturnTy desc ty
56+
57+ ||| Type alias to describe a file operatons that returns a result.
58+ FileOpResult : Type -> Type
59+ FileOpResult ty = FileOpReturnTy RESULT ty
60+
61+ ||| Type alias to describe file oeprations that indicate success.
62+ FileOpSuccess : Type
63+ FileOpSuccess = FileOpReturnTy SUCCESS ()
64+
65+-- ------------------------------------------------------------ [ The Resource ]
66+
67+||| The file handle associated with the effect.
27|||
68|||
28−||| empty; read; write; // States
69+||| @m The `Mode` that the handle was generated under.
70+data FileHandle : (m : Mode) -> Type where
71+ FH : File -> FileHandle m
72+
73+-- ---------------------------------------------- [ Resource Type Construction ]
74+
75+||| Calculates the type for the resource being computed over. `Unit`
76+||| to describe pre-and-post file handle acquisistion, and `FileHandle
77+||| m` when a file handle has been aqcuired.
29|||
78|||
30−||| empty -> read [label="Open R"];
79+||| @m The mode the file handle was generated under.
31−||| read -> empty [label="Close"];
80+||| @ty The functions return type.
32−||| read -> read [label="ReadLine"];
81+calcResourceTy : (m : Mode)
33−||| read -> read [label="EOF"];
82+ -> (ty : FileOpReturnTy fOpTy retTy)
83+ -> Type
84+calcResourceTy _ (FError e) = ()
85+calcResourceTy m _ = FileHandle m
86+
87+-- ------------------------------------------------------- [ Effect Definition ]
88+
89+||| An effect to describe operations on a file.
90+data FileE : Effect where
91+
92+ -- Open/Close
93+
94+ Open : (fname : String)
95+ -> (m : Mode)
96+ -> sig FileE
97+ (FileOpSuccess)
98+ ()
99+ (\res => calcResourceTy m res)
100+
101+ OpenX : (fname : String)
102+ -> (m : Mode)
103+ -> sig FileE
104+ (FileOpSuccess)
105+ ()
106+ (\res => calcResourceTy m res)
107+
108+ Close : sig FileE () (FileHandle m) ()
109+
110+ -- Read
111+
112+ FGetC : {auto prf : ValidModeRead m}
113+ -> sig FileE
114+ (FileOpResult Char)
115+ (FileHandle m)
116+ (FileHandle m)
117+
118+ FGetLine : {auto prf : ValidModeRead m}
119+ -> sig FileE
120+ (FileOpResult String)
121+ (FileHandle m)
122+ (FileHandle m)
123+
124+ FReadFile : (fname : String)
125+ -> sig FileE
126+ (FileOpResult String)
127+ ()
128+ ()
129+ -- Write
130+ FPutStr : (str : String)
131+ -> {auto prf : ValidModeWrite m}
132+ -> sig FileE
133+ (FileOpSuccess)
134+ (FileHandle m)
135+ (FileHandle m)
136+
137+ FPutStrLn : (str : String)
138+ -> {auto prf : ValidModeWrite m}
139+ -> sig FileE
140+ (FileOpSuccess)
141+ (FileHandle m)
142+ (FileHandle m)
143+
144+ FWriteFile : (fname : String)
145+ -> (contents : String)
146+ -> sig FileE
147+ (FileOpSuccess)
148+ ()
149+
150+ -- Flush
151+ FFlush : sig FileE
152+ ()
153+ (FileHandle m)
154+ (FileHandle m)
155+
156+ -- Query
157+ FEOF : {auto prf : ValidModeRead m}
158+ -> sig FileE
159+ Bool
160+ (FileHandle m)
161+
162+-- ---------------------------------------------------------------------- [ IO ]
163+
164+Handler FileE IO where
165+
166+ -- Open Close
167+ handle () (Open fname m) k = do
168+ res <- openFile fname m
169+ case res of
170+ Left err => k (FError err) ()
171+ Right fh => k Success (FH fh)
172+
173+ handle () (OpenX fname m) k = do
174+ res <- openFileX fname m
175+ case res of
176+ Left err => k (FError err) ()
177+ Right fh => k Success (FH fh)
178+
179+ handle (FH h) Close k = do
180+ closeFile h
181+ k () ()
182+
183+ -- Read
184+ handle (FH h) FGetC k = do
185+ res <- fgetc h
186+ case res of
187+ Left err => k (FError err) (FH h)
188+ Right c => k (Result c) (FH h)
189+
190+ handle (FH h) FGetLine k = do
191+ res <- fGetLine h
192+ case res of
193+ Left err => k (FError err) (FH h)
194+ Right ln => k (Result ln) (FH h)
195+
196+ handle () (FReadFile fname) k = do
197+ res <- readFile fname
198+ case res of
199+ Left err => k (FError err) ()
200+ Right str => k (Result str) ()
201+
202+ -- Write
203+ handle (FH fh) (FPutStr str) k = do
204+ res <- fPutStr fh str
205+ case res of
206+ Left err => k (FError err) (FH fh)
207+ Right () => k Success (FH fh)
208+
209+ handle (FH fh) (FPutStrLn str) k = do
210+ res <- fPutStr fh str
211+ case res of
212+ Left err => k (FError err) (FH fh)
213+ Right () => k Success (FH fh)
214+
215+ handle () (FWriteFile fname str) k = do
216+ res <- writeFile fname str
217+ case res of
218+ Left err => k (FError err) ()
219+ Right () => k Success ()
220+
221+ -- Flush
222+ handle (FH fh) FFlush k = do
223+ fflush fh
224+ k () (FH fh)
225+
226+ -- Query
227+ handle (FH fh) FEOF k = do
228+ res <- fEOF fh
229+ k res (FH fh)
230+
231+-- ---------------------------------------------------------------- [ IOExcept ]
232+
233+Handler FileE (IOExcept a) where
234+
235+ -- Open Close
236+ handle () (Open fname m) k = do
237+ res <- ioe_lift $ openFile fname m
238+ case res of
239+ Left err => k (FError err) ()
240+ Right fh => k Success (FH fh)
241+
242+ handle () (OpenX fname m) k = do
243+ res <- ioe_lift $ openFileX fname m
244+ case res of
245+ Left err => k (FError err) ()
246+ Right fh => k Success (FH fh)
247+
248+ handle (FH h) Close k = do
249+ ioe_lift $ closeFile h
250+ k () ()
251+
252+ -- Read
253+ handle (FH h) FGetC k = do
254+ res <- ioe_lift $ fgetc h
255+ case res of
256+ Left err => k (FError err) (FH h)
257+ Right c => k (Result c) (FH h)
258+
259+ handle (FH h) FGetLine k = do
260+ res <- ioe_lift $ fGetLine h
261+ case res of
262+ Left err => k (FError err) (FH h)
263+ Right ln => k (Result ln) (FH h)
264+
265+ handle () (FReadFile fname) k = do
266+ res <- ioe_lift $ readFile fname
267+ case res of
268+ Left err => k (FError err) ()
269+ Right str => k (Result str) ()
270+
271+ -- Write
272+ handle (FH fh) (FPutStr str) k = do
273+ res <- ioe_lift $ fPutStr fh str
274+ case res of
275+ Left err => k (FError err) (FH fh)
276+ Right () => k Success (FH fh)
277+
278+ handle (FH fh) (FPutStrLn str) k = do
279+ res <- ioe_lift $ fPutStr fh str
280+ case res of
281+ Left err => k (FError err) (FH fh)
282+ Right () => k Success (FH fh)
283+
284+ handle () (FWriteFile fname str) k = do
285+ res <- ioe_lift $ writeFile fname str
286+ case res of
287+ Left err => k (FError err) ()
288+ Right () => k Success ()
289+
290+ -- Flush
291+ handle (FH fh) FFlush k = do
292+ ioe_lift $ fflush fh
293+ k () (FH fh)
294+
295+
296+ -- Query
297+ handle (FH fh) FEOF k = do
298+ res <- ioe_lift $ fEOF fh
299+ k res (FH fh)
300+
301+-- ------------------------------------------------------ [ Effect and Helpers ]
302+
303+||| Effectful operations for interacting with files.
34|||
304|||
35−||| empty -> write [label="Open W"];
305+||| The `FILE` effect is parameterised by a file handle once a handle has been acquired, and Unit (`()`) if the file handle is expected to be released once the function has returned.
36−||| write -> empty [label="Close"];
37−||| write -> write [label="WriteLine"];
38|||
306|||
39−||| }
307+FILE : (ty : Type) -> EFFECT
40−data FileIO : Effect where
308+FILE t = MkEff t FileE
41− ||| Open a file with the specified mode.
42− |||
43− ||| Opening a file successful moves the state from 'empty' to the
44− ||| specified mode. If not successful the state is still 'empty'.
45− |||
46− ||| @ fname The file name to be opened.
47− ||| @ m The file mode.
48− Open : (fname: String)
49− -> (m : Mode)
50− -> sig FileIO Bool () (\res => case res of
51− True => OpenFile m
52− False => ())
53−
54− ||| Close a file.
55− |||
56− ||| Closing a file moves the state from Open to closed.
57− Close : sig FileIO () (OpenFile m) ()
58
309
59− ||| Read a line from the file.
310+||| A file has been opened for reading.
60− |||
311+R : Type
61− ||| Only files that are open for reading can be read.
312+R = FileHandle Read
62− ReadLine : sig FileIO String (OpenFile Read)
63
313
64− ||| Write a string to a file.
314+||| A file has been opened for writing.
65− |||
315+W : Type
66− ||| Only file that are open for writing can be written to.
316+W = FileHandle WriteTruncate
67− WriteString : String -> sig FileIO () (OpenFile WriteTruncate)
68
317
69− ||| End of file?
318+||| A file can only be appeneded to.
70− |||
319+A : Type
71− ||| Only files open for reading can be tested for EOF
320+A = FileHandle Append
72− EOF : sig FileIO Bool (OpenFile Read)
321+
73−
322+||| A file can be read and written to.
74−-- ------------------------------------------------------------ [ The Handlers ]
323+RW : Type
75−
324+RW = FileHandle ReadWrite
76−--- An implementation of the resource access protocol for the IO Context.
325+
77−implementation Handler FileIO IO where
326+||| A file opened for reading and writing and has been truncated to
78− handle () (Open fname m) k = do Right h <- openFile fname m
327+||| zero if it previsiouly existed.
79− | Left err => k False ()
328+RWPlus : Type
80− k True (FH h)
329+RWPlus = FileHandle ReadWriteTruncate
81− handle (FH h) Close k = do closeFile h
330+
82− k () ()
331+||| A file will read from the beginning and write at the end.
83− handle (FH h) ReadLine k = do Right str <- fGetLine h
332+APlus : Type
84− -- Need proper error handling!
333+APlus = FileHandle ReadAppend
85− | Left err => k "" (FH h)
334+
86− k str (FH h)
335+-- --------------------------------------------------------------------- [ API ]
87− handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
336+
88− | Left err => k () (FH h)
337+-- -------------------------------------------------------- [ Open/Close/Query ]
89− k () (FH h)
338+
90− handle (FH h) EOF k = do e <- fEOF h
91− k e (FH h)
92−
93−implementation Handler FileIO (IOExcept a) where
94− handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m
95− | Left err => k False ()
96− k True (FH h)
97− handle (FH h) Close k = do ioe_lift $ closeFile h
98− k () ()
99− handle (FH h) ReadLine k = do Right str <- ioe_lift $ fGetLine h
100− -- Need proper error handling!
101− | Left err => k "" (FH h)
102− k str (FH h)
103− handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str
104− | Left err => k () (FH h)
105− k () (FH h)
106− handle (FH h) EOF k = do e <- ioe_lift $ fEOF h
107− k e (FH h)
108−
109−-- -------------------------------------------------------------- [ The Effect ]
110−FILE_IO : Type -> EFFECT
111−FILE_IO t = MkEff t FileIO
112−
113−-- ------------------------------------------------------------ [ The Bindings ]
114−--
115−-- Bind the IO context handlers to functions. These functions will run
116−-- in the IO context.
117−--
118−
119−||| Open a file with the specified mode.
339+||| Open a file.
340+|||
341+||| @ fname the filename.
342+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
343+||| ReadWriteTruncate, or ReadAppend
120|||
344|||
121−||| @ fname The file name to be opened.
122−||| @ m The file mode.
123open : (fname : String)
345open : (fname : String)
124− -> (m : Mode)
346+ -> (m : Mode)
125− -> Eff Bool [FILE_IO ()]
347+ -> Eff (FileOpSuccess)
126− (\res => [FILE_IO (case res of
348+ [FILE ()]
127− True => OpenFile m
349+ (\res => [FILE (calcResourceTy m res)])
128− False => ())])
129open f m = call $ Open f m
350open f m = call $ Open f m
130
351
352+||| Open a file using C11 extended modes.
353+|||
354+||| @ fname the filename
355+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
356+||| ReadWriteTruncate, or ReadAppend
357+openX : (fname : String)
358+ -> (m : Mode)
359+ -> Eff (FileOpSuccess)
360+ [FILE ()]
361+ (\res => [FILE (calcResourceTy m res)])
362+openX f m = call $ OpenX f m
131
363
132||| Close a file.
364||| Close a file.
133−close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
365+close : Eff () [FILE (FileHandle m)] [FILE ()]
134−close = call $ Close
366+close = call (Close)
367+
368+||| Have we reached the end of the file.
369+eof : {auto prf : ValidModeRead m}
370+ -> Eff Bool [FILE (FileHandle m)]
371+eof = call FEOF
372+
373+flush : Eff () [FILE (FileHandle m)]
374+flush = call FFlush
135
375
136−||| Read a line from the file.
376+-- -------------------------------------------------------------------- [ Read ]
137−readLine : Eff String [FILE_IO (OpenFile Read)]
138−readLine = call $ ReadLine
139
377
140−||| Write a string to a file.
378+||| Read a `Char`.
141−writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
379+readChar : {auto prf : ValidModeRead m}
142−writeString str = call $ WriteString str
380+ -> Eff (FileOpResult Char)
381+ [FILE (FileHandle m)]
382+readChar = call FGetC
143
383
144−||| Write a line to a file.
384+||| Read a complete line.
145−writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
385+readLine : {auto prf : ValidModeRead m}
146−writeLine str = call $ WriteString (str ++ "\n")
386+ -> Eff (FileOpResult String)
387+ [FILE (FileHandle m)]
388+readLine = call FGetLine
147
389
148−||| End of file?
390+-- ------------------------------------------------------------------- [ Write ]
149−eof : Eff Bool [FILE_IO (OpenFile Read)]
150−eof = call $ EOF
151
391
152−||| Read a complete file, returning a user defined error if
392+||| Write a string to the file.
153−||| unsuccesful.
393+writeString : (str : String)
394+ -> {auto prf : ValidModeWrite m}
395+ -> Eff (FileOpSuccess)
396+ [FILE (FileHandle m)]
397+writeString str = call $ FPutStr str
398+
399+||| Write a complete line to the file.
400+writeLine : (str : String)
401+ -> {auto prf : ValidModeWrite m}
402+ -> Eff (FileOpSuccess)
403+ [FILE (FileHandle m)]
404+writeLine str = call $ FPutStrLn str
405+
406+-- -------------------------------------------------------------- [ Whole File ]
407+
408+||| Read the contents of a file into a string.
154|||
409|||
155−readFile : (errFunc : String -> e)
410+||| This checks the size of
156− -> (fname : String)
411+||| the file before beginning to read, and only reads that many bytes,
157− -> Eff (Either e String) [FILE_IO ()]
412+||| to ensure that it remains a total function if the file is appended
158−readFile errFunc fname = do
413+||| to while being read.
159− case !(open fname Read) of
160− False => pure $ Left (errFunc fname)
161− True => do
162− src <- readAcc ""
163− close
164− pure $ Right src
165− where
166− readAcc : String -> Eff String [FILE_IO (OpenFile Read)]
167− readAcc acc = if (not !(eof))
168− then readAcc (acc ++ !(readLine))
169− else pure acc
170−
171−||| Write a file containing the provided string, returning a user
172−||| defined error if unsuccesful.
173|||
414|||
174−writeFile : (errFunc : String -> e)
415+||| Returns an error if fname is not a normal file.
175− -> (fname : String)
416+readFile : (fname : String)
176− -> (content : String)
417+ -> Eff (FileOpResult String)
177− -> Eff (Either e ()) [FILE_IO ()]
418+ [FILE ()]
178−writeFile errFunc fname content = do
419+readFile fn = call $ FReadFile fn
179− case !(open fname WriteTruncate) of
420+
180− True => do
421+||| Create a file and write contents to the file.
181− writeString content
422+writeFile : (fname : String)
182− close
423+ -> (contents : String)
183− pure $ Right ()
424+ -> Eff (FileOpSuccess)
184− False => pure $ Left (errFunc fname)
425+ [FILE ()]
185−
426+writeFile fn str = call $ FWriteFile fn str
186−
427+
187−namespace Default
188− readFile : String -> Eff (Either String String) [FILE_IO ()]
189− readFile = File.readFile id
190−
191− writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]
192− writeFile = File.writeFile id
193-- --------------------------------------------------------------------- [ EOF ]
428-- --------------------------------------------------------------------- [ EOF ]
src/Idris/Elab/Term.hs+147−94
@@ -2007,15 +2007,27 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2007 getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
2007 getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
2008 getRetTy ty = ty
2008 getRetTy ty = ty
2009
2009
2010+ elabScriptStuck :: Term -> ElabD a
2011+ elabScriptStuck x = lift . tfail $ ElabScriptStuck x
2012+
2013+
2014+ -- Should be dependent
2015+ tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]
2016+ tacTmArgs l t args | length args == l = return args
2017+ | otherwise = elabScriptStuck t -- Probably should be an argument size mismatch internal error
2018+
2019+
2010 -- | Do a step in the reflected elaborator monad. The input is the
2020 -- | Do a step in the reflected elaborator monad. The input is the
2011 -- step, the output is the (reflected) term returned.
2021 -- step, the output is the (reflected) term returned.
2012 runTacTm :: Term -> ElabD Term
2022 runTacTm :: Term -> ElabD Term
2013− runTacTm (unApply -> tac@(P _ n _, args))
2023+ runTacTm tac@(unApply -> (P _ n _, args))
2014− | n == tacN "Prim__Solve", [] <- args
2024+ | n == tacN "Prim__Solve"
2025+ = do ~[] <- tacTmArgs 0 tac args -- patterns are irrefutable because `tacTmArgs` returns lists of exactly the size given to it as first argument
2015− = do solve
2026+ solve
2016 returnUnit
2027 returnUnit
2017− | n == tacN "Prim__Goal", [] <- args
2028+ | n == tacN "Prim__Goal"
2029+ = do ~[] <- tacTmArgs 0 tac args
2018− = do hs <- get_holes
2030+ hs <- get_holes
2019 case hs of
2031 case hs of
2020 (h : _) -> do t <- goal
2032 (h : _) -> do t <- goal
2021 fmap fst . checkClosed $
2033 fmap fst . checkClosed $
@@ -2024,15 +2036,18 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2024 [] -> lift . tfail . Msg $
2036 [] -> lift . tfail . Msg $
2025 "Elaboration is complete. There are no goals."
2037 "Elaboration is complete. There are no goals."
2026
2038
2027− | n == tacN "Prim__Holes", [] <- args
2039+ | n == tacN "Prim__Holes"
2040+ = do ~[] <- tacTmArgs 0 tac args
2028− = do hs <- get_holes
2041+ hs <- get_holes
2029 fmap fst . checkClosed $
2042 fmap fst . checkClosed $
2030 mkList (Var $ reflm "TTName") (map reflectName hs)
2043 mkList (Var $ reflm "TTName") (map reflectName hs)
2031− | n == tacN "Prim__Guess", [] <- args
2044+ | n == tacN "Prim__Guess"
2045+ = do ~[] <- tacTmArgs 0 tac args
2032− = do g <- get_guess
2046+ g <- get_guess
2033 fmap fst . checkClosed $ reflect g
2047 fmap fst . checkClosed $ reflect g
2034− | n == tacN "Prim__LookupTy", [n] <- args
2048+ | n == tacN "Prim__LookupTy"
2049+ = do ~[name] <- tacTmArgs 1 tac args
2035− = do n' <- reifyTTName n
2050+ n' <- reifyTTName name
2036 ctxt <- get_context
2051 ctxt <- get_context
2037 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
2052 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
2038 TyDecl nt ty -> (nt, ty)
2053 TyDecl nt ty -> (nt, ty)
@@ -2053,20 +2068,23 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2053 , raw_apply (Var pairTy) [ Var (reflm "NameType")
2068 , raw_apply (Var pairTy) [ Var (reflm "NameType")
2054 , Var (reflm "TT")]])
2069 , Var (reflm "TT")]])
2055 defs
2070 defs
2056− | n == tacN "Prim__LookupDatatype", [name] <- args
2071+ | n == tacN "Prim__LookupDatatype"
2072+ = do ~[name] <- tacTmArgs 1 tac args
2057− = do n' <- reifyTTName name
2073+ n' <- reifyTTName name
2058 datatypes <- get_datatypes
2074 datatypes <- get_datatypes
2059 ctxt <- get_context
2075 ctxt <- get_context
2060 fmap fst . checkClosed $
2076 fmap fst . checkClosed $
2061 rawList (Var (tacN "Datatype"))
2077 rawList (Var (tacN "Datatype"))
2062 (map reflectDatatype (buildDatatypes ist n'))
2078 (map reflectDatatype (buildDatatypes ist n'))
2063− | n == tacN "Prim__LookupFunDefn", [name] <- args
2079+ | n == tacN "Prim__LookupFunDefn"
2080+ = do ~[name] <- tacTmArgs 1 tac args
2064− = do n' <- reifyTTName name
2081+ n' <- reifyTTName name
2065 fmap fst . checkClosed $
2082 fmap fst . checkClosed $
2066 rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
2083 rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
2067 (map reflectFunDefn (buildFunDefns ist n'))
2084 (map reflectFunDefn (buildFunDefns ist n'))
2068− | n == tacN "Prim__LookupArgs", [name] <- args
2085+ | n == tacN "Prim__LookupArgs"
2086+ = do ~[name] <- tacTmArgs 1 tac args
2069− = do n' <- reifyTTName name
2087+ n' <- reifyTTName name
2070 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
2088 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
2071 listFunArg = RApp listTy (Var (tacN "FunArg"))
2089 listFunArg = RApp listTy (Var (tacN "FunArg"))
2072 -- Idris tuples nest to the right
2090 -- Idris tuples nest to the right
@@ -2089,37 +2107,45 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2089 (Var (tacN "FunArg"))
2107 (Var (tacN "FunArg"))
2090 , Var (reflm "Raw")]])
2108 , Var (reflm "Raw")]])
2091 out
2109 out
2092− | n == tacN "Prim__SourceLocation", [] <- args
2110+ | n == tacN "Prim__SourceLocation"
2111+ = do ~[] <- tacTmArgs 0 tac args
2093− = fmap fst . checkClosed $
2112+ fmap fst . checkClosed $
2094− reflectFC fc
2113+ reflectFC fc
2095− | n == tacN "Prim__Namespace", [] <- args
2114+ | n == tacN "Prim__Namespace"
2115+ = do ~[] <- tacTmArgs 0 tac args
2096− = fmap fst . checkClosed $
2116+ fmap fst . checkClosed $
2097− rawList (RConstant StrType) (map (RConstant . Str) ns)
2117+ rawList (RConstant StrType) (map (RConstant . Str) ns)
2098− | n == tacN "Prim__Env", [] <- args
2118+ | n == tacN "Prim__Env"
2119+ = do ~[] <- tacTmArgs 0 tac args
2099− = do env <- get_env
2120+ env <- get_env
2100 fmap fst . checkClosed $ reflectEnv env
2121 fmap fst . checkClosed $ reflectEnv env
2101− | n == tacN "Prim__Fail", [_a, errs] <- args
2122+ | n == tacN "Prim__Fail"
2123+ = do ~[_a, errs] <- tacTmArgs 2 tac args
2102− = do errs' <- eval errs
2124+ errs' <- eval errs
2103 parts <- reifyReportParts errs'
2125 parts <- reifyReportParts errs'
2104 lift . tfail $ ReflectionError [parts] (Msg "")
2126 lift . tfail $ ReflectionError [parts] (Msg "")
2105− | n == tacN "Prim__PureElab", [_a, tm] <- args
2127+ | n == tacN "Prim__PureElab"
2128+ = do ~[_a, tm] <- tacTmArgs 2 tac args
2106− = return tm
2129+ return tm
2107− | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
2130+ | n == tacN "Prim__BindElab"
2131+ = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args
2108− = do first' <- eval first
2132+ first' <- eval first
2109 res <- eval =<< runTacTm first'
2133 res <- eval =<< runTacTm first'
2110 next <- eval (App Complete andThen res)
2134 next <- eval (App Complete andThen res)
2111 runTacTm next
2135 runTacTm next
2112− | n == tacN "Prim__Try", [_a, first, alt] <- args
2136+ | n == tacN "Prim__Try"
2137+ = do ~[_a, first, alt] <- tacTmArgs 3 tac args
2113− = do first' <- eval first
2138+ first' <- eval first
2114 alt' <- eval alt
2139 alt' <- eval alt
2115 try' (runTacTm first') (runTacTm alt') True
2140 try' (runTacTm first') (runTacTm alt') True
2116− | n == tacN "Prim__Fill", [raw] <- args
2141+ | n == tacN "Prim__Fill"
2142+ = do ~[raw] <- tacTmArgs 1 tac args
2117− = do raw' <- reifyRaw =<< eval raw
2143+ raw' <- reifyRaw =<< eval raw
2118 apply raw' []
2144 apply raw' []
2119 returnUnit
2145 returnUnit
2120 | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
2146 | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
2121− , [raw, argSpec] <- args
2147+ = do ~[raw, argSpec] <- tacTmArgs 2 tac args
2122− = do raw' <- reifyRaw =<< eval raw
2148+ raw' <- reifyRaw =<< eval raw
2123 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
2149 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
2124 let op = if n == tacN "Prim__Apply"
2150 let op = if n == tacN "Prim__Apply"
2125 then apply
2151 then apply
@@ -2131,89 +2157,105 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2131 (reflectName n1, reflectName n2)
2157 (reflectName n1, reflectName n2)
2132 | (n1, n2) <- ns
2158 | (n1, n2) <- ns
2133 ]
2159 ]
2134− | n == tacN "Prim__Gensym", [hint] <- args
2160+ | n == tacN "Prim__Gensym"
2161+ = do ~[hint] <- tacTmArgs 1 tac args
2135− = do hintStr <- eval hint
2162+ hintStr <- eval hint
2136 case hintStr of
2163 case hintStr of
2137 Constant (Str h) -> do
2164 Constant (Str h) -> do
2138 n <- getNameFrom (sMN 0 h)
2165 n <- getNameFrom (sMN 0 h)
2139 fmap fst $ get_type_val (reflectName n)
2166 fmap fst $ get_type_val (reflectName n)
2140 _ -> fail "no hint"
2167 _ -> fail "no hint"
2141− | n == tacN "Prim__Claim", [n, ty] <- args
2168+ | n == tacN "Prim__Claim"
2169+ = do ~[n, ty] <- tacTmArgs 2 tac args
2142− = do n' <- reifyTTName n
2170+ n' <- reifyTTName n
2143 ty' <- reifyRaw ty
2171 ty' <- reifyRaw ty
2144 claim n' ty'
2172 claim n' ty'
2145 returnUnit
2173 returnUnit
2146− | n == tacN "Prim__Check", [env', raw] <- args
2174+ | n == tacN "Prim__Check"
2175+ = do ~[env', raw] <- tacTmArgs 2 tac args
2147− = do env <- reifyEnv env'
2176+ env <- reifyEnv env'
2148 raw' <- reifyRaw =<< eval raw
2177 raw' <- reifyRaw =<< eval raw
2149 ctxt <- get_context
2178 ctxt <- get_context
2150 (tm, ty) <- lift $ check ctxt env raw'
2179 (tm, ty) <- lift $ check ctxt env raw'
2151 fmap fst . checkClosed $
2180 fmap fst . checkClosed $
2152 rawPair (Var (reflm "TT"), Var (reflm "TT"))
2181 rawPair (Var (reflm "TT"), Var (reflm "TT"))
2153 (reflect tm, reflect ty)
2182 (reflect tm, reflect ty)
2154− | n == tacN "Prim__Attack", [] <- args
2183+ | n == tacN "Prim__Attack"
2184+ = do ~[] <- tacTmArgs 0 tac args
2155− = do attack
2185+ attack
2156 returnUnit
2186 returnUnit
2157− | n == tacN "Prim__Rewrite", [rule] <- args
2187+ | n == tacN "Prim__Rewrite"
2188+ = do ~[rule] <- tacTmArgs 1 tac args
2158− = do r <- reifyRaw rule
2189+ r <- reifyRaw rule
2159 rewrite r
2190 rewrite r
2160 returnUnit
2191 returnUnit
2161− | n == tacN "Prim__Focus", [what] <- args
2192+ | n == tacN "Prim__Focus"
2193+ = do ~[what] <- tacTmArgs 1 tac args
2162− = do n' <- reifyTTName what
2194+ n' <- reifyTTName what
2163 hs <- get_holes
2195 hs <- get_holes
2164 if elem n' hs
2196 if elem n' hs
2165 then focus n' >> returnUnit
2197 then focus n' >> returnUnit
2166 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
2198 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
2167− | n == tacN "Prim__Unfocus", [what] <- args
2199+ | n == tacN "Prim__Unfocus"
2200+ = do ~[what] <- tacTmArgs 1 tac args
2168− = do n' <- reifyTTName what
2201+ n' <- reifyTTName what
2169 movelast n'
2202 movelast n'
2170 returnUnit
2203 returnUnit
2171− | n == tacN "Prim__Intro", [mn] <- args
2204+ | n == tacN "Prim__Intro"
2205+ = do ~[mn] <- tacTmArgs 1 tac args
2172− = do n <- case fromTTMaybe mn of
2206+ n <- case fromTTMaybe mn of
2173 Nothing -> return Nothing
2207 Nothing -> return Nothing
2174 Just name -> fmap Just $ reifyTTName name
2208 Just name -> fmap Just $ reifyTTName name
2175 intro n
2209 intro n
2176 returnUnit
2210 returnUnit
2177− | n == tacN "Prim__Forall", [n, ty] <- args
2211+ | n == tacN "Prim__Forall"
2212+ = do ~[n, ty] <- tacTmArgs 2 tac args
2178− = do n' <- reifyTTName n
2213+ n' <- reifyTTName n
2179 ty' <- reifyRaw ty
2214 ty' <- reifyRaw ty
2180 forall n' Nothing ty'
2215 forall n' Nothing ty'
2181 returnUnit
2216 returnUnit
2182− | n == tacN "Prim__PatVar", [n] <- args
2217+ | n == tacN "Prim__PatVar"
2218+ = do ~[n] <- tacTmArgs 1 tac args
2183− = do n' <- reifyTTName n
2219+ n' <- reifyTTName n
2184 patvar' n'
2220 patvar' n'
2185 returnUnit
2221 returnUnit
2186− | n == tacN "Prim__PatBind", [n] <- args
2222+ | n == tacN "Prim__PatBind"
2223+ = do ~[n] <- tacTmArgs 1 tac args
2187− = do n' <- reifyTTName n
2224+ n' <- reifyTTName n
2188 patbind n'
2225 patbind n'
2189 returnUnit
2226 returnUnit
2190− | n == tacN "Prim__LetBind", [n, ty, tm] <- args
2227+ | n == tacN "Prim__LetBind"
2228+ = do ~[n, ty, tm] <- tacTmArgs 3 tac args
2191− = do n' <- reifyTTName n
2229+ n' <- reifyTTName n
2192 ty' <- reifyRaw ty
2230 ty' <- reifyRaw ty
2193 tm' <- reifyRaw tm
2231 tm' <- reifyRaw tm
2194 letbind n' ty' tm'
2232 letbind n' ty' tm'
2195 returnUnit
2233 returnUnit
2196− | n == tacN "Prim__Compute", [] <- args
2234+ | n == tacN "Prim__Compute"
2197− = do compute ; returnUnit
2235+ = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit
2198− | n == tacN "Prim__Normalise", [env, tm] <- args
2236+ | n == tacN "Prim__Normalise"
2237+ = do ~[env, tm] <- tacTmArgs 2 tac args
2199− = do env' <- reifyEnv env
2238+ env' <- reifyEnv env
2200 tm' <- reifyTT tm
2239 tm' <- reifyTT tm
2201 ctxt <- get_context
2240 ctxt <- get_context
2202 let out = normaliseAll ctxt env' (finalise tm')
2241 let out = normaliseAll ctxt env' (finalise tm')
2203 fmap fst . checkClosed $ reflect out
2242 fmap fst . checkClosed $ reflect out
2204− | n == tacN "Prim__Whnf", [tm] <- args
2243+ | n == tacN "Prim__Whnf"
2244+ = do ~[tm] <- tacTmArgs 1 tac args
2205− = do tm' <- reifyTT tm
2245+ tm' <- reifyTT tm
2206 ctxt <- get_context
2246 ctxt <- get_context
2207 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2247 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2208− | n == tacN "Prim__Converts", [env, tm1, tm2] <- args
2248+ | n == tacN "Prim__Converts"
2249+ = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2209− = do env' <- reifyEnv env
2250+ env' <- reifyEnv env
2210 tm1' <- reifyTT tm1
2251 tm1' <- reifyTT tm1
2211 tm2' <- reifyTT tm2
2252 tm2' <- reifyTT tm2
2212 ctxt <- get_context
2253 ctxt <- get_context
2213 lift $ converts ctxt env' tm1' tm2'
2254 lift $ converts ctxt env' tm1' tm2'
2214 returnUnit
2255 returnUnit
2215− | n == tacN "Prim__DeclareType", [decl] <- args
2256+ | n == tacN "Prim__DeclareType"
2257+ = do ~[decl] <- tacTmArgs 1 tac args
2216− = do (RDeclare n args res) <- reifyTyDecl decl
2258+ (RDeclare n args res) <- reifyTyDecl decl
2217 ctxt <- get_context
2259 ctxt <- get_context
2218 let rty = foldr mkPi res args
2260 let rty = foldr mkPi res args
2219 (checked, ty') <- lift $ check ctxt [] rty
2261 (checked, ty') <- lift $ check ctxt [] rty
@@ -2225,12 +2267,14 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2225 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
2267 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
2226 new_tyDecls e }
2268 new_tyDecls e }
2227 returnUnit
2269 returnUnit
2228− | n == tacN "Prim__DefineFunction", [decl] <- args
2270+ | n == tacN "Prim__DefineFunction"
2271+ = do ~[decl] <- tacTmArgs 1 tac args
2229− = do defn <- reifyFunDefn decl
2272+ defn <- reifyFunDefn decl
2230 defineFunction defn
2273 defineFunction defn
2231 returnUnit
2274 returnUnit
2232− | n == tacN "Prim__DeclareDatatype", [decl] <- args
2275+ | n == tacN "Prim__DeclareDatatype"
2276+ = do ~[decl] <- tacTmArgs 1 tac args
2233− = do RDeclare n args resTy <- reifyTyDecl decl
2277+ RDeclare n args resTy <- reifyTyDecl decl
2234 ctxt <- get_context
2278 ctxt <- get_context
2235 let tcTy = foldr mkPi resTy args
2279 let tcTy = foldr mkPi resTy args
2236 (checked, ty') <- lift $ check ctxt [] tcTy
2280 (checked, ty') <- lift $ check ctxt [] tcTy
@@ -2240,8 +2284,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2240 set_context ctxt'
2284 set_context ctxt'
2241 updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
2285 updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
2242 returnUnit
2286 returnUnit
2243− | n == tacN "Prim__DefineDatatype", [defn] <- args
2287+ | n == tacN "Prim__DefineDatatype"
2288+ = do ~[defn] <- tacTmArgs 1 tac args
2244− = do RDefineDatatype n ctors <- reifyRDataDefn defn
2289+ RDefineDatatype n ctors <- reifyRDataDefn defn
2245 ctxt <- get_context
2290 ctxt <- get_context
2246 tyconTy <- case lookupTyExact n ctxt of
2291 tyconTy <- case lookupTyExact n ctxt of
2247 Just t -> return t
2292 Just t -> return t
@@ -2264,24 +2309,28 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2264 -- the rest happens in a bit
2309 -- the rest happens in a bit
2265 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
2310 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
2266 returnUnit
2311 returnUnit
2267− | n == tacN "Prim__AddInstance", [cls, inst] <- args
2312+ | n == tacN "Prim__AddInstance"
2313+ = do ~[cls, inst] <- tacTmArgs 2 tac args
2268− = do className <- reifyTTName cls
2314+ className <- reifyTTName cls
2269 instName <- reifyTTName inst
2315 instName <- reifyTTName inst
2270 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2316 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2271 new_tyDecls e }
2317 new_tyDecls e }
2272 returnUnit
2318 returnUnit
2273− | n == tacN "Prim__IsTCName", [n] <- args
2319+ | n == tacN "Prim__IsTCName"
2320+ = do ~[n] <- tacTmArgs 1 tac args
2274− = do n' <- reifyTTName n
2321+ n' <- reifyTTName n
2275 case lookupCtxtExact n' (idris_classes ist) of
2322 case lookupCtxtExact n' (idris_classes ist) of
2276 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2323 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2277 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2324 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2278− | n == tacN "Prim__ResolveTC", [fn] <- args
2325+ | n == tacN "Prim__ResolveTC"
2326+ = do ~[fn] <- tacTmArgs 1 tac args
2279− = do g <- goal
2327+ g <- goal
2280 fn <- reifyTTName fn
2328 fn <- reifyTTName fn
2281 resolveTC' False True 100 g fn ist
2329 resolveTC' False True 100 g fn ist
2282 returnUnit
2330 returnUnit
2283− | n == tacN "Prim__Search", [depth, hints] <- args
2331+ | n == tacN "Prim__Search"
2332+ = do ~[depth, hints] <- tacTmArgs 2 tac args
2284− = do d <- eval depth
2333+ d <- eval depth
2285 hints' <- eval hints
2334 hints' <- eval hints
2286 case (d, unList hints') of
2335 case (d, unList hints') of
2287 (Constant (I i), Just hs) ->
2336 (Constant (I i), Just hs) ->
@@ -2293,8 +2342,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2293 (Constant (I _), Nothing ) ->
2342 (Constant (I _), Nothing ) ->
2294 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
2343 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
2295 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2344 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2296− | n == tacN "Prim__RecursiveElab", [goal, script] <- args
2345+ | n == tacN "Prim__RecursiveElab"
2346+ = do ~[goal, script] <- tacTmArgs 2 tac args
2297− = do goal' <- reifyRaw goal
2347+ goal' <- reifyRaw goal
2298 ctxt <- get_context
2348 ctxt <- get_context
2299 script <- eval script
2349 script <- eval script
2300 (goalTT, goalTy) <- lift $ check ctxt [] goal'
2350 (goalTT, goalTy) <- lift $ check ctxt [] goal'
@@ -2327,8 +2377,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2327 fmap fst . checkClosed $
2377 fmap fst . checkClosed $
2328 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2378 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2329 (tm', ty')
2379 (tm', ty')
2330− | n == tacN "Prim__Metavar", [n] <- args
2380+ | n == tacN "Prim__Metavar"
2381+ = do ~[n] <- tacTmArgs 1 tac args
2331− = do n' <- reifyTTName n
2382+ n' <- reifyTTName n
2332 ctxt <- get_context
2383 ctxt <- get_context
2333 ptm <- get_term
2384 ptm <- get_term
2334 -- See documentation above in the elab case for PMetavar
2385 -- See documentation above in the elab case for PMetavar
@@ -2338,8 +2389,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2338 defer unique_used mvn
2389 defer unique_used mvn
2339 solve
2390 solve
2340 returnUnit
2391 returnUnit
2341− | n == tacN "Prim__Fixity", [op'] <- args
2392+ | n == tacN "Prim__Fixity"
2393+ = do ~[op'] <- tacTmArgs 1 tac args
2342− = do opTm <- eval op'
2394+ opTm <- eval op'
2343 case opTm of
2395 case opTm of
2344 Constant (Str op) ->
2396 Constant (Str op) ->
2345 let opChars = ":!#$%&*+./<=>?@\\^|-~"
2397 let opChars = ":!#$%&*+./<=>?@\\^|-~"
@@ -2352,11 +2404,12 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2352 [f] -> fmap fst . checkClosed $ reflectFixity f
2404 [f] -> fmap fst . checkClosed $ reflectFixity f
2353 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
2405 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
2354 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2406 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2355− | n == tacN "Prim__Debug", [ty, msg] <- args
2407+ | n == tacN "Prim__Debug"
2408+ = do ~[ty, msg] <- tacTmArgs 2 tac args
2356− = do msg' <- eval msg
2409+ msg' <- eval msg
2357 parts <- reifyReportParts msg
2410 parts <- reifyReportParts msg
2358 debugElaborator parts
2411 debugElaborator parts
2359− runTacTm x = lift . tfail $ ElabScriptStuck x
2412+ runTacTm x = elabScriptStuck x
2360
2413
2361-- Running tactics directly
2414-- Running tactics directly
2362-- if a tactic adds unification problems, return an error
2415-- if a tactic adds unification problems, return an error
test/effects001/test021.idr+35−21
@@ -8,27 +8,41 @@ import Control.IOExcept
8
8
9data Count : Type where
9data Count : Type where
10
10
11−FileIO : Type -> Type -> Type
12−FileIO st t = Eff t [FILE_IO st, STDIO, Count ::: STATE Int]
13
11
14−readFile : FileIO (OpenFile Read) (List String)
12+TestFileIO : Type -> Type -> Type
13+TestFileIO st t = Eff t [FILE st, STDIO, Count ::: STATE Int]
14+
15+readFileCount : Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
16+readFileCount = readAcc []
15−readFile = readAcc [] where
17+ where
16− readAcc : List String -> FileIO (OpenFile Read) (List String)
18+ readAcc : List String
19+ -> Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
17− readAcc acc = do e <- eof
20+ readAcc acc = do
21+ e <- eof
18− if (not e)
22+ if (not e)
23+ then do
19− then do str <- readLine
24+ (Result str) <- readLine
25+ | (FError err) => pure (FError err)
20− Count :- put (!(Count :- get) + 1)
26+ Count :- put (!(Count :- get) + 1)
21− readAcc (str :: acc)
27+ readAcc (str :: acc)
28+ else do
22− else return (reverse acc)
29+ let res = reverse acc
23−
30+ pure $ Result res
31+
24−testFile : FileIO () ()
32+testFile : TestFileIO () ()
33+testFile = do
25−testFile = do True <- open "testFile" Read | False => putStrLn "Error!"
34+ Success <- open "testFile" Read
35+ | (FError err) => do
36+ putStrLn "Error!"
37+ pure ()
26− fcontents <- readFile
38+ (Result fcontents) <- readFileCount
39+ | (FError err) => do
40+ close
41+ putStrLn "Error!"
42+ pure ()
27− putStrLn (show fcontents)
43+ putStrLn (show fcontents)
28− close
44+ close
29− putStrLn (show !(Count :- get))
45+ putStrLn (show !(Count :- get))
30
46
31main : IO ()
47main : IO ()
32−main = run testFile
48+main = run testFile
33−
34−
test/runtest.hs+1
@@ -130,6 +130,7 @@ runTest conf test = do
130 -- that depend on that distinction in other contexts.
130 -- that depend on that distinction in other contexts.
131 -- Also rewrite newlines for consistency.
131 -- Also rewrite newlines for consistency.
132 norm ('\r':'\n':xs) = '\n' : norm xs
132 norm ('\r':'\n':xs) = '\n' : norm xs
133+ norm ('\\':'\\':xs) = '/' : norm xs
133 norm ('\\':xs) = '/' : norm xs
134 norm ('\\':xs) = '/' : norm xs
134 norm (x : xs) = x : norm xs
135 norm (x : xs) = x : norm xs
135 norm [] = []
136 norm [] = []