git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit5a8ca144dfd80dcb9ee2a24b0fa3a231d2783ad8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 4 Jul 2016, 17:07 (10 years ago) parentf3a4971e99330b
6 files changed+671−277
compare with master
unifiedsplit
CHANGELOG.md+2 docs/tutorial/typesfuns.rst+89 libs/effects/Effect/File.idr+397−162 src/Idris/Elab/Term.hs+147−94 test/effects001/test021.idr+35−21 test/runtest.hs+1
CHANGELOG.md+2
@@ -20,6 +20,8 @@
2020 correct st = record { score->correct $= (+1),
2121 score->attempted $= (+1) } st
2222 ```
23+* The File Effect has been updated to take into account changes in
24+ `Prelude.File` and to provide a 'better' API.
2325
2426# New in 0.12:
2527
docs/tutorial/typesfuns.rst+89
@@ -685,6 +685,95 @@ without any explicit use of ``Force`` or ``Delay``:
685685 ifThenElse True t e = t;
686686 ifThenElse False t e = e;
687687
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+
688777Useful Data Types
689778=================
690779
libs/effects/Effect/File.idr+397−162
@@ -1,4 +1,4 @@
1−-- -------------------------------------------------------- [ Effectful FileIO ]
1+||| Effectful file operations.
22module Effect.File
33
44import Effects
@@ -6,188 +6,423 @@ import Control.IOExcept
66
77%access public export
88
9−||| A Dependent type to describe File Handles. File handles are
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
9+-- -------------------------------------------------------------- [ Predicates ]
1610
17−openOK : Mode -> Bool -> Type
18−openOK m True = OpenFile m
19−openOK m False = ()
11+||| A record of the file modes that can read from a file.
12+data ValidModeRead : Mode -> Type where
13+ VMRRead : ValidModeRead Read
14+ VMRReadW : ValidModeRead ReadWrite
15+ VMRReadWT : ValidModeRead ReadWriteTruncate
16+ VMRReadA : ValidModeRead ReadAppend
2017
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
2224
23−||| Here the protocol for resource access is defined as an effect.
24−||| The state transitions diagram for the protocol is as follows:
25−|||
26−||| digraph G {
25+-- -------------------------------------------------- [ Custom Error Reporting ]
26+
27+namespace FileResult
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.
2768|||
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.
2978|||
30−||| empty -> read [label="Open R"];
31−||| read -> empty [label="Close"];
32−||| read -> read [label="ReadLine"];
33−||| read -> read [label="EOF"];
79+||| @m The mode the file handle was generated under.
80+||| @ty The functions return type.
81+calcResourceTy : (m : Mode)
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.
34304|||
35−||| empty -> write [label="Open W"];
36−||| write -> empty [label="Close"];
37−||| write -> write [label="WriteLine"];
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.
38306|||
39−||| }
40−data FileIO : Effect where
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) ()
307+FILE : (ty : Type) -> EFFECT
308+FILE t = MkEff t FileE
58309
59− ||| Read a line from the file.
60− |||
61− ||| Only files that are open for reading can be read.
62− ReadLine : sig FileIO String (OpenFile Read)
310+||| A file has been opened for reading.
311+R : Type
312+R = FileHandle Read
63313
64− ||| Write a string to a file.
65− |||
66− ||| Only file that are open for writing can be written to.
67− WriteString : String -> sig FileIO () (OpenFile WriteTruncate)
314+||| A file has been opened for writing.
315+W : Type
316+W = FileHandle WriteTruncate
68317
69− ||| End of file?
70− |||
71− ||| Only files open for reading can be tested for EOF
72− EOF : sig FileIO Bool (OpenFile Read)
73−
74−-- ------------------------------------------------------------ [ The Handlers ]
75−
76−--- An implementation of the resource access protocol for the IO Context.
77−implementation Handler FileIO IO where
78− handle () (Open fname m) k = do Right h <- openFile fname m
79− | Left err => k False ()
80− k True (FH h)
81− handle (FH h) Close k = do closeFile h
82− k () ()
83− handle (FH h) ReadLine k = do Right str <- fGetLine h
84− -- Need proper error handling!
85− | Left err => k "" (FH h)
86− k str (FH h)
87− handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
88− | Left err => k () (FH h)
89− k () (FH h)
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.
318+||| A file can only be appeneded to.
319+A : Type
320+A = FileHandle Append
321+
322+||| A file can be read and written to.
323+RW : Type
324+RW = FileHandle ReadWrite
325+
326+||| A file opened for reading and writing and has been truncated to
327+||| zero if it previsiouly existed.
328+RWPlus : Type
329+RWPlus = FileHandle ReadWriteTruncate
330+
331+||| A file will read from the beginning and write at the end.
332+APlus : Type
333+APlus = FileHandle ReadAppend
334+
335+-- --------------------------------------------------------------------- [ API ]
336+
337+-- -------------------------------------------------------- [ Open/Close/Query ]
338+
339+||| Open a file.
340+|||
341+||| @ fname the filename.
342+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,
343+||| ReadWriteTruncate, or ReadAppend
120344|||
121−||| @ fname The file name to be opened.
122−||| @ m The file mode.
123345open : (fname : String)
124− -> (m : Mode)
125− -> Eff Bool [FILE_IO ()]
126− (\res => [FILE_IO (case res of
127− True => OpenFile m
128− False => ())])
346+ -> (m : Mode)
347+ -> Eff (FileOpSuccess)
348+ [FILE ()]
349+ (\res => [FILE (calcResourceTy m res)])
129350open f m = call $ Open f m
130351
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
131363
132364||| Close a file.
133−close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
134−close = call $ Close
365+close : Eff () [FILE (FileHandle m)] [FILE ()]
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
135375
136−||| Read a line from the file.
137−readLine : Eff String [FILE_IO (OpenFile Read)]
138−readLine = call $ ReadLine
376+-- -------------------------------------------------------------------- [ Read ]
139377
140−||| Write a string to a file.
141−writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
142−writeString str = call $ WriteString str
378+||| Read a `Char`.
379+readChar : {auto prf : ValidModeRead m}
380+ -> Eff (FileOpResult Char)
381+ [FILE (FileHandle m)]
382+readChar = call FGetC
143383
144−||| Write a line to a file.
145−writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
146−writeLine str = call $ WriteString (str ++ "\n")
384+||| Read a complete line.
385+readLine : {auto prf : ValidModeRead m}
386+ -> Eff (FileOpResult String)
387+ [FILE (FileHandle m)]
388+readLine = call FGetLine
147389
148−||| End of file?
149−eof : Eff Bool [FILE_IO (OpenFile Read)]
150−eof = call $ EOF
390+-- ------------------------------------------------------------------- [ Write ]
151391
152−||| Read a complete file, returning a user defined error if
153−||| unsuccesful.
392+||| Write a string to the file.
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.
154409|||
155−readFile : (errFunc : String -> e)
156− -> (fname : String)
157− -> Eff (Either e String) [FILE_IO ()]
158−readFile errFunc fname = do
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.
410+||| This checks the size of
411+||| the file before beginning to read, and only reads that many bytes,
412+||| to ensure that it remains a total function if the file is appended
413+||| to while being read.
173414|||
174−writeFile : (errFunc : String -> e)
175− -> (fname : String)
176− -> (content : String)
177− -> Eff (Either e ()) [FILE_IO ()]
178−writeFile errFunc fname content = do
179− case !(open fname WriteTruncate) of
180− True => do
181− writeString content
182− close
183− pure $ Right ()
184− False => pure $ Left (errFunc fname)
185−
186−
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
415+||| Returns an error if fname is not a normal file.
416+readFile : (fname : String)
417+ -> Eff (FileOpResult String)
418+ [FILE ()]
419+readFile fn = call $ FReadFile fn
420+
421+||| Create a file and write contents to the file.
422+writeFile : (fname : String)
423+ -> (contents : String)
424+ -> Eff (FileOpSuccess)
425+ [FILE ()]
426+writeFile fn str = call $ FWriteFile fn str
427+
193428-- --------------------------------------------------------------------- [ EOF ]
src/Idris/Elab/Term.hs+147−94
@@ -2007,15 +2007,27 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20072007 getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
20082008 getRetTy ty = ty
20092009
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+
20102020 -- | Do a step in the reflected elaborator monad. The input is the
20112021 -- step, the output is the (reflected) term returned.
20122022 runTacTm :: Term -> ElabD Term
2013− runTacTm (unApply -> tac@(P _ n _, args))
2014− | n == tacN "Prim__Solve", [] <- args
2015− = do solve
2023+ runTacTm tac@(unApply -> (P _ n _, 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
2026+ solve
20162027 returnUnit
2017− | n == tacN "Prim__Goal", [] <- args
2018− = do hs <- get_holes
2028+ | n == tacN "Prim__Goal"
2029+ = do ~[] <- tacTmArgs 0 tac args
2030+ hs <- get_holes
20192031 case hs of
20202032 (h : _) -> do t <- goal
20212033 fmap fst . checkClosed $
@@ -2024,15 +2036,18 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20242036 [] -> lift . tfail . Msg $
20252037 "Elaboration is complete. There are no goals."
20262038
2027− | n == tacN "Prim__Holes", [] <- args
2028− = do hs <- get_holes
2039+ | n == tacN "Prim__Holes"
2040+ = do ~[] <- tacTmArgs 0 tac args
2041+ hs <- get_holes
20292042 fmap fst . checkClosed $
20302043 mkList (Var $ reflm "TTName") (map reflectName hs)
2031− | n == tacN "Prim__Guess", [] <- args
2032− = do g <- get_guess
2044+ | n == tacN "Prim__Guess"
2045+ = do ~[] <- tacTmArgs 0 tac args
2046+ g <- get_guess
20332047 fmap fst . checkClosed $ reflect g
2034− | n == tacN "Prim__LookupTy", [n] <- args
2035− = do n' <- reifyTTName n
2048+ | n == tacN "Prim__LookupTy"
2049+ = do ~[name] <- tacTmArgs 1 tac args
2050+ n' <- reifyTTName name
20362051 ctxt <- get_context
20372052 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
20382053 TyDecl nt ty -> (nt, ty)
@@ -2053,20 +2068,23 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20532068 , raw_apply (Var pairTy) [ Var (reflm "NameType")
20542069 , Var (reflm "TT")]])
20552070 defs
2056− | n == tacN "Prim__LookupDatatype", [name] <- args
2057− = do n' <- reifyTTName name
2071+ | n == tacN "Prim__LookupDatatype"
2072+ = do ~[name] <- tacTmArgs 1 tac args
2073+ n' <- reifyTTName name
20582074 datatypes <- get_datatypes
20592075 ctxt <- get_context
20602076 fmap fst . checkClosed $
20612077 rawList (Var (tacN "Datatype"))
20622078 (map reflectDatatype (buildDatatypes ist n'))
2063− | n == tacN "Prim__LookupFunDefn", [name] <- args
2064− = do n' <- reifyTTName name
2079+ | n == tacN "Prim__LookupFunDefn"
2080+ = do ~[name] <- tacTmArgs 1 tac args
2081+ n' <- reifyTTName name
20652082 fmap fst . checkClosed $
20662083 rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
20672084 (map reflectFunDefn (buildFunDefns ist n'))
2068− | n == tacN "Prim__LookupArgs", [name] <- args
2069− = do n' <- reifyTTName name
2085+ | n == tacN "Prim__LookupArgs"
2086+ = do ~[name] <- tacTmArgs 1 tac args
2087+ n' <- reifyTTName name
20702088 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
20712089 listFunArg = RApp listTy (Var (tacN "FunArg"))
20722090 -- Idris tuples nest to the right
@@ -2089,37 +2107,45 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20892107 (Var (tacN "FunArg"))
20902108 , Var (reflm "Raw")]])
20912109 out
2092− | n == tacN "Prim__SourceLocation", [] <- args
2093− = fmap fst . checkClosed $
2094− reflectFC fc
2095− | n == tacN "Prim__Namespace", [] <- args
2096− = fmap fst . checkClosed $
2097− rawList (RConstant StrType) (map (RConstant . Str) ns)
2098− | n == tacN "Prim__Env", [] <- args
2099− = do env <- get_env
2110+ | n == tacN "Prim__SourceLocation"
2111+ = do ~[] <- tacTmArgs 0 tac args
2112+ fmap fst . checkClosed $
2113+ reflectFC fc
2114+ | n == tacN "Prim__Namespace"
2115+ = do ~[] <- tacTmArgs 0 tac args
2116+ fmap fst . checkClosed $
2117+ rawList (RConstant StrType) (map (RConstant . Str) ns)
2118+ | n == tacN "Prim__Env"
2119+ = do ~[] <- tacTmArgs 0 tac args
2120+ env <- get_env
21002121 fmap fst . checkClosed $ reflectEnv env
2101− | n == tacN "Prim__Fail", [_a, errs] <- args
2102− = do errs' <- eval errs
2122+ | n == tacN "Prim__Fail"
2123+ = do ~[_a, errs] <- tacTmArgs 2 tac args
2124+ errs' <- eval errs
21032125 parts <- reifyReportParts errs'
21042126 lift . tfail $ ReflectionError [parts] (Msg "")
2105− | n == tacN "Prim__PureElab", [_a, tm] <- args
2106− = return tm
2107− | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
2108− = do first' <- eval first
2127+ | n == tacN "Prim__PureElab"
2128+ = do ~[_a, tm] <- tacTmArgs 2 tac args
2129+ return tm
2130+ | n == tacN "Prim__BindElab"
2131+ = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args
2132+ first' <- eval first
21092133 res <- eval =<< runTacTm first'
21102134 next <- eval (App Complete andThen res)
21112135 runTacTm next
2112− | n == tacN "Prim__Try", [_a, first, alt] <- args
2113− = do first' <- eval first
2136+ | n == tacN "Prim__Try"
2137+ = do ~[_a, first, alt] <- tacTmArgs 3 tac args
2138+ first' <- eval first
21142139 alt' <- eval alt
21152140 try' (runTacTm first') (runTacTm alt') True
2116− | n == tacN "Prim__Fill", [raw] <- args
2117− = do raw' <- reifyRaw =<< eval raw
2141+ | n == tacN "Prim__Fill"
2142+ = do ~[raw] <- tacTmArgs 1 tac args
2143+ raw' <- reifyRaw =<< eval raw
21182144 apply raw' []
21192145 returnUnit
21202146 | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
2121− , [raw, argSpec] <- args
2122− = do raw' <- reifyRaw =<< eval raw
2147+ = do ~[raw, argSpec] <- tacTmArgs 2 tac args
2148+ raw' <- reifyRaw =<< eval raw
21232149 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
21242150 let op = if n == tacN "Prim__Apply"
21252151 then apply
@@ -2131,89 +2157,105 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
21312157 (reflectName n1, reflectName n2)
21322158 | (n1, n2) <- ns
21332159 ]
2134− | n == tacN "Prim__Gensym", [hint] <- args
2135− = do hintStr <- eval hint
2160+ | n == tacN "Prim__Gensym"
2161+ = do ~[hint] <- tacTmArgs 1 tac args
2162+ hintStr <- eval hint
21362163 case hintStr of
21372164 Constant (Str h) -> do
21382165 n <- getNameFrom (sMN 0 h)
21392166 fmap fst $ get_type_val (reflectName n)
21402167 _ -> fail "no hint"
2141− | n == tacN "Prim__Claim", [n, ty] <- args
2142− = do n' <- reifyTTName n
2168+ | n == tacN "Prim__Claim"
2169+ = do ~[n, ty] <- tacTmArgs 2 tac args
2170+ n' <- reifyTTName n
21432171 ty' <- reifyRaw ty
21442172 claim n' ty'
21452173 returnUnit
2146− | n == tacN "Prim__Check", [env', raw] <- args
2147− = do env <- reifyEnv env'
2174+ | n == tacN "Prim__Check"
2175+ = do ~[env', raw] <- tacTmArgs 2 tac args
2176+ env <- reifyEnv env'
21482177 raw' <- reifyRaw =<< eval raw
21492178 ctxt <- get_context
21502179 (tm, ty) <- lift $ check ctxt env raw'
21512180 fmap fst . checkClosed $
21522181 rawPair (Var (reflm "TT"), Var (reflm "TT"))
21532182 (reflect tm, reflect ty)
2154− | n == tacN "Prim__Attack", [] <- args
2155− = do attack
2183+ | n == tacN "Prim__Attack"
2184+ = do ~[] <- tacTmArgs 0 tac args
2185+ attack
21562186 returnUnit
2157− | n == tacN "Prim__Rewrite", [rule] <- args
2158− = do r <- reifyRaw rule
2187+ | n == tacN "Prim__Rewrite"
2188+ = do ~[rule] <- tacTmArgs 1 tac args
2189+ r <- reifyRaw rule
21592190 rewrite r
21602191 returnUnit
2161− | n == tacN "Prim__Focus", [what] <- args
2162− = do n' <- reifyTTName what
2192+ | n == tacN "Prim__Focus"
2193+ = do ~[what] <- tacTmArgs 1 tac args
2194+ n' <- reifyTTName what
21632195 hs <- get_holes
21642196 if elem n' hs
21652197 then focus n' >> returnUnit
21662198 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
2167− | n == tacN "Prim__Unfocus", [what] <- args
2168− = do n' <- reifyTTName what
2199+ | n == tacN "Prim__Unfocus"
2200+ = do ~[what] <- tacTmArgs 1 tac args
2201+ n' <- reifyTTName what
21692202 movelast n'
21702203 returnUnit
2171− | n == tacN "Prim__Intro", [mn] <- args
2172− = do n <- case fromTTMaybe mn of
2204+ | n == tacN "Prim__Intro"
2205+ = do ~[mn] <- tacTmArgs 1 tac args
2206+ n <- case fromTTMaybe mn of
21732207 Nothing -> return Nothing
21742208 Just name -> fmap Just $ reifyTTName name
21752209 intro n
21762210 returnUnit
2177− | n == tacN "Prim__Forall", [n, ty] <- args
2178− = do n' <- reifyTTName n
2211+ | n == tacN "Prim__Forall"
2212+ = do ~[n, ty] <- tacTmArgs 2 tac args
2213+ n' <- reifyTTName n
21792214 ty' <- reifyRaw ty
21802215 forall n' Nothing ty'
21812216 returnUnit
2182− | n == tacN "Prim__PatVar", [n] <- args
2183− = do n' <- reifyTTName n
2217+ | n == tacN "Prim__PatVar"
2218+ = do ~[n] <- tacTmArgs 1 tac args
2219+ n' <- reifyTTName n
21842220 patvar' n'
21852221 returnUnit
2186− | n == tacN "Prim__PatBind", [n] <- args
2187− = do n' <- reifyTTName n
2222+ | n == tacN "Prim__PatBind"
2223+ = do ~[n] <- tacTmArgs 1 tac args
2224+ n' <- reifyTTName n
21882225 patbind n'
21892226 returnUnit
2190− | n == tacN "Prim__LetBind", [n, ty, tm] <- args
2191− = do n' <- reifyTTName n
2227+ | n == tacN "Prim__LetBind"
2228+ = do ~[n, ty, tm] <- tacTmArgs 3 tac args
2229+ n' <- reifyTTName n
21922230 ty' <- reifyRaw ty
21932231 tm' <- reifyRaw tm
21942232 letbind n' ty' tm'
21952233 returnUnit
2196− | n == tacN "Prim__Compute", [] <- args
2197− = do compute ; returnUnit
2198− | n == tacN "Prim__Normalise", [env, tm] <- args
2199− = do env' <- reifyEnv env
2234+ | n == tacN "Prim__Compute"
2235+ = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit
2236+ | n == tacN "Prim__Normalise"
2237+ = do ~[env, tm] <- tacTmArgs 2 tac args
2238+ env' <- reifyEnv env
22002239 tm' <- reifyTT tm
22012240 ctxt <- get_context
22022241 let out = normaliseAll ctxt env' (finalise tm')
22032242 fmap fst . checkClosed $ reflect out
2204− | n == tacN "Prim__Whnf", [tm] <- args
2205− = do tm' <- reifyTT tm
2243+ | n == tacN "Prim__Whnf"
2244+ = do ~[tm] <- tacTmArgs 1 tac args
2245+ tm' <- reifyTT tm
22062246 ctxt <- get_context
22072247 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2208− | n == tacN "Prim__Converts", [env, tm1, tm2] <- args
2209− = do env' <- reifyEnv env
2248+ | n == tacN "Prim__Converts"
2249+ = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2250+ env' <- reifyEnv env
22102251 tm1' <- reifyTT tm1
22112252 tm2' <- reifyTT tm2
22122253 ctxt <- get_context
22132254 lift $ converts ctxt env' tm1' tm2'
22142255 returnUnit
2215− | n == tacN "Prim__DeclareType", [decl] <- args
2216− = do (RDeclare n args res) <- reifyTyDecl decl
2256+ | n == tacN "Prim__DeclareType"
2257+ = do ~[decl] <- tacTmArgs 1 tac args
2258+ (RDeclare n args res) <- reifyTyDecl decl
22172259 ctxt <- get_context
22182260 let rty = foldr mkPi res args
22192261 (checked, ty') <- lift $ check ctxt [] rty
@@ -2225,12 +2267,14 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22252267 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
22262268 new_tyDecls e }
22272269 returnUnit
2228− | n == tacN "Prim__DefineFunction", [decl] <- args
2229− = do defn <- reifyFunDefn decl
2270+ | n == tacN "Prim__DefineFunction"
2271+ = do ~[decl] <- tacTmArgs 1 tac args
2272+ defn <- reifyFunDefn decl
22302273 defineFunction defn
22312274 returnUnit
2232− | n == tacN "Prim__DeclareDatatype", [decl] <- args
2233− = do RDeclare n args resTy <- reifyTyDecl decl
2275+ | n == tacN "Prim__DeclareDatatype"
2276+ = do ~[decl] <- tacTmArgs 1 tac args
2277+ RDeclare n args resTy <- reifyTyDecl decl
22342278 ctxt <- get_context
22352279 let tcTy = foldr mkPi resTy args
22362280 (checked, ty') <- lift $ check ctxt [] tcTy
@@ -2240,8 +2284,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22402284 set_context ctxt'
22412285 updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
22422286 returnUnit
2243− | n == tacN "Prim__DefineDatatype", [defn] <- args
2244− = do RDefineDatatype n ctors <- reifyRDataDefn defn
2287+ | n == tacN "Prim__DefineDatatype"
2288+ = do ~[defn] <- tacTmArgs 1 tac args
2289+ RDefineDatatype n ctors <- reifyRDataDefn defn
22452290 ctxt <- get_context
22462291 tyconTy <- case lookupTyExact n ctxt of
22472292 Just t -> return t
@@ -2264,24 +2309,28 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22642309 -- the rest happens in a bit
22652310 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
22662311 returnUnit
2267− | n == tacN "Prim__AddInstance", [cls, inst] <- args
2268− = do className <- reifyTTName cls
2312+ | n == tacN "Prim__AddInstance"
2313+ = do ~[cls, inst] <- tacTmArgs 2 tac args
2314+ className <- reifyTTName cls
22692315 instName <- reifyTTName inst
22702316 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
22712317 new_tyDecls e }
22722318 returnUnit
2273− | n == tacN "Prim__IsTCName", [n] <- args
2274− = do n' <- reifyTTName n
2319+ | n == tacN "Prim__IsTCName"
2320+ = do ~[n] <- tacTmArgs 1 tac args
2321+ n' <- reifyTTName n
22752322 case lookupCtxtExact n' (idris_classes ist) of
22762323 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
22772324 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2278− | n == tacN "Prim__ResolveTC", [fn] <- args
2279− = do g <- goal
2325+ | n == tacN "Prim__ResolveTC"
2326+ = do ~[fn] <- tacTmArgs 1 tac args
2327+ g <- goal
22802328 fn <- reifyTTName fn
22812329 resolveTC' False True 100 g fn ist
22822330 returnUnit
2283− | n == tacN "Prim__Search", [depth, hints] <- args
2284− = do d <- eval depth
2331+ | n == tacN "Prim__Search"
2332+ = do ~[depth, hints] <- tacTmArgs 2 tac args
2333+ d <- eval depth
22852334 hints' <- eval hints
22862335 case (d, unList hints') of
22872336 (Constant (I i), Just hs) ->
@@ -2293,8 +2342,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22932342 (Constant (I _), Nothing ) ->
22942343 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
22952344 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2296− | n == tacN "Prim__RecursiveElab", [goal, script] <- args
2297− = do goal' <- reifyRaw goal
2345+ | n == tacN "Prim__RecursiveElab"
2346+ = do ~[goal, script] <- tacTmArgs 2 tac args
2347+ goal' <- reifyRaw goal
22982348 ctxt <- get_context
22992349 script <- eval script
23002350 (goalTT, goalTy) <- lift $ check ctxt [] goal'
@@ -2327,8 +2377,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
23272377 fmap fst . checkClosed $
23282378 rawPair (Var $ reflm "TT", Var $ reflm "TT")
23292379 (tm', ty')
2330− | n == tacN "Prim__Metavar", [n] <- args
2331− = do n' <- reifyTTName n
2380+ | n == tacN "Prim__Metavar"
2381+ = do ~[n] <- tacTmArgs 1 tac args
2382+ n' <- reifyTTName n
23322383 ctxt <- get_context
23332384 ptm <- get_term
23342385 -- See documentation above in the elab case for PMetavar
@@ -2338,8 +2389,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
23382389 defer unique_used mvn
23392390 solve
23402391 returnUnit
2341− | n == tacN "Prim__Fixity", [op'] <- args
2342− = do opTm <- eval op'
2392+ | n == tacN "Prim__Fixity"
2393+ = do ~[op'] <- tacTmArgs 1 tac args
2394+ opTm <- eval op'
23432395 case opTm of
23442396 Constant (Str op) ->
23452397 let opChars = ":!#$%&*+./<=>?@\\^|-~"
@@ -2352,11 +2404,12 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
23522404 [f] -> fmap fst . checkClosed $ reflectFixity f
23532405 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
23542406 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2355− | n == tacN "Prim__Debug", [ty, msg] <- args
2356− = do msg' <- eval msg
2407+ | n == tacN "Prim__Debug"
2408+ = do ~[ty, msg] <- tacTmArgs 2 tac args
2409+ msg' <- eval msg
23572410 parts <- reifyReportParts msg
23582411 debugElaborator parts
2359− runTacTm x = lift . tfail $ ElabScriptStuck x
2412+ runTacTm x = elabScriptStuck x
23602413
23612414-- Running tactics directly
23622415-- if a tactic adds unification problems, return an error
test/effects001/test021.idr+35−21
@@ -8,27 +8,41 @@ import Control.IOExcept
88
99data Count : Type where
1010
11−FileIO : Type -> Type -> Type
12−FileIO st t = Eff t [FILE_IO st, STDIO, Count ::: STATE Int]
1311
14−readFile : FileIO (OpenFile Read) (List String)
15−readFile = readAcc [] where
16− readAcc : List String -> FileIO (OpenFile Read) (List String)
17− readAcc acc = do e <- eof
18− if (not e)
19− then do str <- readLine
20− Count :- put (!(Count :- get) + 1)
21− readAcc (str :: acc)
22− else return (reverse acc)
23−
24−testFile : FileIO () ()
25−testFile = do True <- open "testFile" Read | False => putStrLn "Error!"
26− fcontents <- readFile
27− putStrLn (show fcontents)
28− close
29− putStrLn (show !(Count :- get))
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 []
17+ where
18+ readAcc : List String
19+ -> Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
20+ readAcc acc = do
21+ e <- eof
22+ if (not e)
23+ then do
24+ (Result str) <- readLine
25+ | (FError err) => pure (FError err)
26+ Count :- put (!(Count :- get) + 1)
27+ readAcc (str :: acc)
28+ else do
29+ let res = reverse acc
30+ pure $ Result res
31+
32+testFile : TestFileIO () ()
33+testFile = do
34+ Success <- open "testFile" Read
35+ | (FError err) => do
36+ putStrLn "Error!"
37+ pure ()
38+ (Result fcontents) <- readFileCount
39+ | (FError err) => do
40+ close
41+ putStrLn "Error!"
42+ pure ()
43+ putStrLn (show fcontents)
44+ close
45+ putStrLn (show !(Count :- get))
3046
3147main : IO ()
32−main = run testFile
33−
34−
48+main = run testFile
test/runtest.hs+1
@@ -130,6 +130,7 @@ runTest conf test = do
130130 -- that depend on that distinction in other contexts.
131131 -- Also rewrite newlines for consistency.
132132 norm ('\r':'\n':xs) = '\n' : norm xs
133+ norm ('\\':'\\':xs) = '/' : norm xs
133134 norm ('\\':xs) = '/' : norm xs
134135 norm (x : xs) = x : norm xs
135136 norm [] = []