idris 0.12 → 0.12.1
raw patch · 58 files changed
+1432/−1498 lines, 58 filesdep +arraydep +regex-tdfadep ~binarydep ~processdep ~time
Dependencies added: array, regex-tdfa
Dependency ranges changed: binary, process, time, transformers, trifecta
Files
- CHANGELOG.md +33/−0
- CONTRIBUTORS +7/−5
- idris.cabal +30/−6
- libs/base/Control/Monad/RWS.idr +1/−1
- libs/base/Control/Monad/Reader.idr +1/−1
- libs/base/Control/Monad/State.idr +16/−16
- libs/base/Control/Monad/Writer.idr +1/−1
- libs/effects/Effect/File.idr +389/−154
- libs/prelude/Builtins.idr +2/−3
- libs/prelude/Prelude/Traversable.idr +8/−0
- rts/idris_rts.c +3/−0
- src/IRTS/CodegenCommon.hs +4/−1
- src/IRTS/CodegenJavaScript.hs +44/−9
- src/IRTS/Compiler.hs +2/−2
- src/IRTS/Lang.hs +27/−2
- src/Idris/AbsSyntaxTree.hs +46/−40
- src/Idris/CaseSplit.hs +2/−2
- src/Idris/Colours.hs +3/−1
- src/Idris/Core/CaseTree.hs +40/−26
- src/Idris/Core/DeepSeq.hs +37/−278
- src/Idris/Core/Evaluate.hs +23/−9
- src/Idris/Core/ProofState.hs +3/−1
- src/Idris/Core/TT.hs +28/−27
- src/Idris/Coverage.hs +3/−2
- src/Idris/DeepSeq.hs +59/−680
- src/Idris/Delaborate.hs +34/−13
- src/Idris/Docs.hs +55/−42
- src/Idris/Docstrings.hs +6/−6
- src/Idris/Elab/Clause.hs +5/−2
- src/Idris/Elab/Term.hs +172/−112
- src/Idris/IBC.hs +1/−1
- src/Idris/Parser.hs +2/−2
- src/Idris/Parser/Expr.hs +17/−8
- src/Idris/Parser/Helpers.hs +15/−0
- src/Idris/Prover.hs +3/−3
- src/Idris/REPL.hs +13/−13
- src/Pkg/PParser.hs +15/−1
- src/Util/DynamicLinker.hs +67/−6
- stack.yaml +3/−2
- test/docs004/docs004.idr +11/−0
- test/docs004/expected +18/−0
- test/docs004/input +3/−0
- test/docs004/run +3/−0
- test/docs005/docs005.idr +19/−0
- test/docs005/expected +29/−0
- test/docs005/input +2/−0
- test/docs005/run +3/−0
- test/effects001/test021.idr +34/−20
- test/interfaces006/expected +0/−0
- test/interfaces006/interfaces006.idr +19/−0
- test/interfaces006/run +3/−0
- test/records004/expected +3/−0
- test/records004/records004.idr +13/−0
- test/records004/run +4/−0
- test/records005/expected +4/−0
- test/records005/records005.idr +39/−0
- test/records005/run +4/−0
- test/runtest.hs +1/−0
CHANGELOG.md view
@@ -1,3 +1,36 @@+# New in 0.13:++## Language updates++* `record` syntax now allows updating fields, including nested fields,+ by applying a function using the `$=` operator. For example:++ ```+ record Score where+ constructor MkScore+ correct : Nat+ attempted : Nat++ record GameState where+ constructor MkGameState+ score : Score+ difficulty : Nat++ correct : GameState -> GameState+ correct st = record { score->correct $= (+1),+ score->attempted $= (+1) } st+ ```++## Library updates++* The File Effect has been updated to take into account changes in+ `Prelude.File` and to provide a 'better' API.++## Tool updates++* Idris' documentation system now displays the documentation for auto+ implicits in the output of `:doc`. This is tested for in `docs005`.+ # New in 0.12: ## Language updates
CONTRIBUTORS view
@@ -3,20 +3,22 @@ Ozgur Akgun Ahmad Salim Al-Sibahi Edward Chadwick Amsden-Jan Bessai Michael R. Bernstein+Jan Bessai Nicola Botta Edwin Brady Jakob Brünker Alyssa Carter-David Raymond Christiansen Carter Charbonneau+David Raymond Christiansen Aaron Craelius Jason Dagit+Adam Sandberg Eriksson Guglielmo Fachini Simon Fowler Google Zack Grannan+Sean Hunt Cezar Ionescu Heath Johns Irene Knapp@@ -27,14 +29,14 @@ Hannes Mehnert Mekeor Melire Melissa Mozifian-Dominic Mulligan Jan de Muijnck-Hughes+Dominic Mulligan+Echo Nolan Tom Prince raichoo Philip Rasmussen Aistis Raulinaitis Reynir Reynisson-Adam Sandberg Eriksson Seo Sanghyeon Benjamin Saunders Alexander Shabalin@@ -47,5 +49,5 @@ Dirk Ullrich Leif Warner Daniel Waterworth+Eric Weinstein Jonas Westerlund-Sean Hunt
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.12+Version: 0.12.1 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -580,6 +580,9 @@ test/interfaces005/*.idr test/interfaces005/run test/interfaces005/expected+ test/interfaces006/*.idr+ test/interfaces006/run+ test/interfaces006/expected test/io001/run test/io001/*.idr@@ -708,6 +711,12 @@ test/records003/run test/records003/*.idr test/records003/expected+ test/records004/run+ test/records004/*.idr+ test/records004/expected+ test/records005/run+ test/records005/*.idr+ test/records005/expected test/sourceLocation001/run test/sourceLocation001/*.idr@@ -849,7 +858,16 @@ test/docs003/input test/docs003/*.idr test/docs003/expected+ test/docs004/run+ test/docs004/input+ test/docs004/*.idr+ test/docs004/expected+ test/docs005/run+ test/docs005/input+ test/docs005/*.idr+ test/docs005/expected + benchmarks/ALL benchmarks/*.pl benchmarks/README@@ -1026,8 +1044,9 @@ , annotated-wl-pprint >= 0.7 && < 0.8 , ansi-terminal < 0.7 , ansi-wl-pprint < 0.7+ , array >= 0.4.0.1 && < 0.6 , base64-bytestring < 1.1- , binary >= 0.7 && < 0.8+ , binary >= 0.7 && < 0.9 , blaze-html >= 0.6.1.3 && < 0.9 , blaze-markup >= 0.5.2.1 && < 0.8 , bytestring < 0.11@@ -1044,14 +1063,14 @@ , optparse-applicative >= 0.11 && < 0.13 , parsers >= 0.9 && < 0.13 , pretty < 1.2- , process < 1.3+ , regex-tdfa >= 1.2 , split < 0.3 , terminal-size < 0.4 , text >=1.2.1.0 && < 1.3- , time >= 1.4 && < 1.6- , transformers < 0.5+ , time >= 1.4 && < 1.7+ , transformers < 0.6 , transformers-compat >= 0.3- , trifecta >= 1.1 && < 1.6+ , trifecta >= 1.6 && < 1.7 , uniplate >=1.6 && < 1.7 , unordered-containers < 0.3 , utf8-string < 1.1@@ -1062,9 +1081,14 @@ , fsnotify >= 0.2 && < 2.2 , async < 2.2 + -- zlib >= 0.6.1 is broken with GHC < 7.10.3+ -- Travis is broken for 7.6 and 7.8 with a newer process if impl(ghc < 7.10.3) build-depends: zlib < 0.6.1+ , process < 1.3+ else+ build-depends: process < 1.5 Extensions: MultiParamTypeClasses , DeriveFoldable
libs/base/Control/Monad/RWS.idr view
@@ -8,7 +8,7 @@ %access public export ||| A combination of the Reader, Writer, and State monads-interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}+interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) | m where {} ||| The transformer on which the RWS monad is based record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
libs/base/Control/Monad/Reader.idr view
@@ -7,7 +7,7 @@ %access public export ||| A monad representing a computation that runs in an immutable context-interface Monad m => MonadReader r (m : Type -> Type) where+interface Monad m => MonadReader r (m : Type -> Type) | m where ||| Return the context ask : m r ||| Temprorarily modify the input and run an action in the new context
libs/base/Control/Monad/State.idr view
@@ -6,64 +6,64 @@ %access public export ||| A computation which runs in a context and produces an output-interface Monad m => MonadState s (m : Type -> Type) | m where+interface Monad m => MonadState stateType (m : Type -> Type) | m where ||| Get the context- get : m s+ get : m stateType ||| Write a new context/output- put : s -> m ()+ put : stateType -> m () ||| The transformer on which the State monad is based-record StateT (s : Type) (m : Type -> Type) (a : Type) where+record StateT (stateType : Type) (m : Type -> Type) (a : Type) where constructor ST- runStateT : s -> m (a, s)+ runStateT : stateType -> m (a, stateType) -implementation Functor f => Functor (StateT s f) where+implementation Functor f => Functor (StateT stateType f) where map f (ST g) = ST (\st => map (mapFst f) (g st)) where mapFst : (a -> x) -> (a, s) -> (x, s) mapFst fn (a, b) = (fn a, b) -implementation Monad f => Applicative (StateT s f) where+implementation Monad f => Applicative (StateT stateType f) where pure x = ST (\st => pure (x, st)) (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st (b, t) <- a r return (g b, t)) -implementation Monad m => Monad (StateT s m) where+implementation Monad m => Monad (StateT stateType m) where (ST f) >>= k = ST (\st => do (v, st') <- f st let ST kv = k v kv st') -implementation Monad m => MonadState s (StateT s m) where+implementation Monad m => MonadState stateType (StateT stateType m) where get = ST (\x => return (x, x)) put x = ST (\y => return ((), x)) -implementation MonadTrans (StateT s) where+implementation MonadTrans (StateT stateType) where lift x = ST (\st => do r <- x return (r, st)) ||| Apply a function to modify the context of this computation-modify : MonadState s m => (s -> s) -> m ()+modify : MonadState stateType m => (stateType -> stateType) -> m () modify f = do s <- get put (f s) ||| Evaluate a function in the context held by this computation-gets : MonadState s m => (s -> a) -> m a+gets : MonadState stateType m => (stateType -> a) -> m a gets f = do s <- get return (f s) ||| The State monad. See the MonadState interface-State : Type -> Type -> Type+State : (stateType : Type) -> (ty : Type) -> Type State = \s, a => StateT s Identity a ||| Unwrap a State monad computation.-runState : StateT s Identity a -> s -> (a, s)+runState : StateT stateType Identity a -> stateType -> (a, stateType) runState act = runIdentity . runStateT act ||| Unwrap a State monad computation, but discard the final state.-evalState : State s a -> s -> a+evalState : State stateType a -> stateType -> a evalState m = fst . runState m ||| Unwrap a State monad computation, but discard the resulting value.-execState : State s a -> s -> s+execState : State stateType a -> stateType -> stateType execState m = snd . runState m
libs/base/Control/Monad/Writer.idr view
@@ -7,7 +7,7 @@ %access public export ||| A monad representing a computation that produces a stream of output-interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where+interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) | m where ||| tell w produces the output w tell : w -> m () ||| Execute an action and add it's output to the value of the computation
libs/effects/Effect/File.idr view
@@ -1,4 +1,4 @@--- -------------------------------------------------------- [ Effectful FileIO ]+||| Effectful file operations. module Effect.File import Effects@@ -6,188 +6,423 @@ %access public export -||| A Dependent type to describe File Handles. File handles are-||| parameterised with the current state of the file: Closed; Open for-||| reading; and Open for writing.-|||-||| @ m The file mode.-data OpenFile : (m : Mode) -> Type where- FH : File -> OpenFile m+-- -------------------------------------------------------------- [ Predicates ] -openOK : Mode -> Bool -> Type-openOK m True = OpenFile m-openOK m False = ()+||| A record of the file modes that can read from a file.+data ValidModeRead : Mode -> Type where+ VMRRead : ValidModeRead Read+ VMRReadW : ValidModeRead ReadWrite+ VMRReadWT : ValidModeRead ReadWriteTruncate+ VMRReadA : ValidModeRead ReadAppend --- ------------------------------------------------------------ [ The Protocol ]+||| A record of the file modes that can write from a file.+data ValidModeWrite : Mode -> Type where+ VMWWrite : ValidModeWrite WriteTruncate+ VMWAppend : ValidModeWrite Append+ VMWReadW : ValidModeWrite ReadWrite+ VMWReadWT : ValidModeWrite ReadWriteTruncate -||| Here the protocol for resource access is defined as an effect.-||| The state transitions diagram for the protocol is as follows:-|||-||| digraph G {+-- -------------------------------------------------- [ Custom Error Reporting ]++namespace FileResult++ ||| A type to describe the return type of file operations.+ data ResultDesc = SUCCESS | RESULT++ ||| A custom return type for file operations that is dependent on+ ||| the type of file operation.+ |||+ ||| @desc Parameterises the constructors to describe if the function+ ||| returns a value or not.+ ||| @ty The return type for a file operation that returns a value.+ |||+ data FileOpReturnTy : (desc : ResultDesc)+ -> (ty : Type)+ -> Type where++ ||| The operation completed successfully and doesn't return a+ ||| result.+ Success : FileOpReturnTy SUCCESS ty++ ||| The operation returns a result of type `ty`.+ |||+ ||| @ty The value returned.+ Result : ty -> FileOpReturnTy RESULT ty++ ||| The operation failed and the RTS produced the given error.+ |||+ ||| @err The reported error code.+ FError : (err : FileError) -> FileOpReturnTy desc ty++ ||| Type alias to describe a file operatons that returns a result.+ FileOpResult : Type -> Type+ FileOpResult ty = FileOpReturnTy RESULT ty++ ||| Type alias to describe file oeprations that indicate success.+ FileOpSuccess : Type+ FileOpSuccess = FileOpReturnTy SUCCESS ()++-- ------------------------------------------------------------ [ The Resource ]++||| The file handle associated with the effect. |||-||| empty; read; write; // States+||| @m The `Mode` that the handle was generated under.+data FileHandle : (m : Mode) -> Type where+ FH : File -> FileHandle m++-- ---------------------------------------------- [ Resource Type Construction ]++||| Calculates the type for the resource being computed over. `Unit`+||| to describe pre-and-post file handle acquisistion, and `FileHandle+||| m` when a file handle has been aqcuired. |||-||| empty -> read [label="Open R"];-||| read -> empty [label="Close"];-||| read -> read [label="ReadLine"];-||| read -> read [label="EOF"];+||| @m The mode the file handle was generated under.+||| @ty The functions return type.+calcResourceTy : (m : Mode)+ -> (ty : FileOpReturnTy fOpTy retTy)+ -> Type+calcResourceTy _ (FError e) = ()+calcResourceTy m _ = FileHandle m++-- ------------------------------------------------------- [ Effect Definition ]++||| An effect to describe operations on a file.+data FileE : Effect where++ -- Open/Close++ Open : (fname : String)+ -> (m : Mode)+ -> sig FileE+ (FileOpSuccess)+ ()+ (\res => calcResourceTy m res)++ OpenX : (fname : String)+ -> (m : Mode)+ -> sig FileE+ (FileOpSuccess)+ ()+ (\res => calcResourceTy m res)++ Close : sig FileE () (FileHandle m) ()++ -- Read++ FGetC : {auto prf : ValidModeRead m}+ -> sig FileE+ (FileOpResult Char)+ (FileHandle m)+ (FileHandle m)++ FGetLine : {auto prf : ValidModeRead m}+ -> sig FileE+ (FileOpResult String)+ (FileHandle m)+ (FileHandle m)++ FReadFile : (fname : String)+ -> sig FileE+ (FileOpResult String)+ ()+ ()+ -- Write+ FPutStr : (str : String)+ -> {auto prf : ValidModeWrite m}+ -> sig FileE+ (FileOpSuccess)+ (FileHandle m)+ (FileHandle m)++ FPutStrLn : (str : String)+ -> {auto prf : ValidModeWrite m}+ -> sig FileE+ (FileOpSuccess)+ (FileHandle m)+ (FileHandle m)++ FWriteFile : (fname : String)+ -> (contents : String)+ -> sig FileE+ (FileOpSuccess)+ ()++ -- Flush+ FFlush : sig FileE+ ()+ (FileHandle m)+ (FileHandle m)++ -- Query+ FEOF : {auto prf : ValidModeRead m}+ -> sig FileE+ Bool+ (FileHandle m)++-- ---------------------------------------------------------------------- [ IO ]++Handler FileE IO where++ -- Open Close+ handle () (Open fname m) k = do+ res <- openFile fname m+ case res of+ Left err => k (FError err) ()+ Right fh => k Success (FH fh)++ handle () (OpenX fname m) k = do+ res <- openFileX fname m+ case res of+ Left err => k (FError err) ()+ Right fh => k Success (FH fh)++ handle (FH h) Close k = do+ closeFile h+ k () ()++ -- Read+ handle (FH h) FGetC k = do+ res <- fgetc h+ case res of+ Left err => k (FError err) (FH h)+ Right c => k (Result c) (FH h)++ handle (FH h) FGetLine k = do+ res <- fGetLine h+ case res of+ Left err => k (FError err) (FH h)+ Right ln => k (Result ln) (FH h)++ handle () (FReadFile fname) k = do+ res <- readFile fname+ case res of+ Left err => k (FError err) ()+ Right str => k (Result str) ()++ -- Write+ handle (FH fh) (FPutStr str) k = do+ res <- fPutStr fh str+ case res of+ Left err => k (FError err) (FH fh)+ Right () => k Success (FH fh)++ handle (FH fh) (FPutStrLn str) k = do+ res <- fPutStr fh str+ case res of+ Left err => k (FError err) (FH fh)+ Right () => k Success (FH fh)++ handle () (FWriteFile fname str) k = do+ res <- writeFile fname str+ case res of+ Left err => k (FError err) ()+ Right () => k Success ()++ -- Flush+ handle (FH fh) FFlush k = do+ fflush fh+ k () (FH fh)++ -- Query+ handle (FH fh) FEOF k = do+ res <- fEOF fh+ k res (FH fh)++-- ---------------------------------------------------------------- [ IOExcept ]++Handler FileE (IOExcept a) where++ -- Open Close+ handle () (Open fname m) k = do+ res <- ioe_lift $ openFile fname m+ case res of+ Left err => k (FError err) ()+ Right fh => k Success (FH fh)++ handle () (OpenX fname m) k = do+ res <- ioe_lift $ openFileX fname m+ case res of+ Left err => k (FError err) ()+ Right fh => k Success (FH fh)++ handle (FH h) Close k = do+ ioe_lift $ closeFile h+ k () ()++ -- Read+ handle (FH h) FGetC k = do+ res <- ioe_lift $ fgetc h+ case res of+ Left err => k (FError err) (FH h)+ Right c => k (Result c) (FH h)++ handle (FH h) FGetLine k = do+ res <- ioe_lift $ fGetLine h+ case res of+ Left err => k (FError err) (FH h)+ Right ln => k (Result ln) (FH h)++ handle () (FReadFile fname) k = do+ res <- ioe_lift $ readFile fname+ case res of+ Left err => k (FError err) ()+ Right str => k (Result str) ()++ -- Write+ handle (FH fh) (FPutStr str) k = do+ res <- ioe_lift $ fPutStr fh str+ case res of+ Left err => k (FError err) (FH fh)+ Right () => k Success (FH fh)++ handle (FH fh) (FPutStrLn str) k = do+ res <- ioe_lift $ fPutStr fh str+ case res of+ Left err => k (FError err) (FH fh)+ Right () => k Success (FH fh)++ handle () (FWriteFile fname str) k = do+ res <- ioe_lift $ writeFile fname str+ case res of+ Left err => k (FError err) ()+ Right () => k Success ()++ -- Flush+ handle (FH fh) FFlush k = do+ ioe_lift $ fflush fh+ k () (FH fh)+++ -- Query+ handle (FH fh) FEOF k = do+ res <- ioe_lift $ fEOF fh+ k res (FH fh)++-- ------------------------------------------------------ [ Effect and Helpers ]++||| Effectful operations for interacting with files. |||-||| empty -> write [label="Open W"];-||| write -> empty [label="Close"];-||| write -> write [label="WriteLine"];+||| 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. |||-||| }-data FileIO : Effect where- ||| Open a file with the specified mode.- |||- ||| Opening a file successful moves the state from 'empty' to the- ||| specified mode. If not successful the state is still 'empty'.- |||- ||| @ fname The file name to be opened.- ||| @ m The file mode.- Open : (fname: String)- -> (m : Mode)- -> sig FileIO Bool () (\res => case res of- True => OpenFile m- False => ())-- ||| Close a file.- |||- ||| Closing a file moves the state from Open to closed.- Close : sig FileIO () (OpenFile m) ()+FILE : (ty : Type) -> EFFECT+FILE t = MkEff t FileE - ||| Read a line from the file.- |||- ||| Only files that are open for reading can be read.- ReadLine : sig FileIO String (OpenFile Read)+||| A file has been opened for reading.+R : Type+R = FileHandle Read - ||| Write a string to a file.- |||- ||| Only file that are open for writing can be written to.- WriteString : String -> sig FileIO () (OpenFile WriteTruncate)+||| A file has been opened for writing.+W : Type+W = FileHandle WriteTruncate - ||| End of file?- |||- ||| Only files open for reading can be tested for EOF- EOF : sig FileIO Bool (OpenFile Read)+||| A file can only be appeneded to.+A : Type+A = FileHandle Append --- ------------------------------------------------------------ [ The Handlers ]+||| A file can be read and written to.+RW : Type+RW = FileHandle ReadWrite ---- An implementation of the resource access protocol for the IO Context.-implementation Handler FileIO IO where- handle () (Open fname m) k = do Right h <- openFile fname m- | Left err => k False ()- k True (FH h)- handle (FH h) Close k = do closeFile h- k () ()- handle (FH h) ReadLine k = do Right str <- fGetLine h- -- Need proper error handling!- | Left err => k "" (FH h)- k str (FH h)- handle (FH h) (WriteString str) k = do Right () <- fPutStr h str- | Left err => k () (FH h)- k () (FH h)- handle (FH h) EOF k = do e <- fEOF h- k e (FH h)+||| A file opened for reading and writing and has been truncated to+||| zero if it previsiouly existed.+RWPlus : Type+RWPlus = FileHandle ReadWriteTruncate -implementation Handler FileIO (IOExcept a) where- handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m- | Left err => k False ()- k True (FH h)- handle (FH h) Close k = do ioe_lift $ closeFile h- k () ()- handle (FH h) ReadLine k = do Right str <- ioe_lift $ fGetLine h- -- Need proper error handling!- | Left err => k "" (FH h)- k str (FH h)- handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str- | Left err => k () (FH h)- k () (FH h)- handle (FH h) EOF k = do e <- ioe_lift $ fEOF h- k e (FH h)+||| A file will read from the beginning and write at the end.+APlus : Type+APlus = FileHandle ReadAppend --- -------------------------------------------------------------- [ The Effect ]-FILE_IO : Type -> EFFECT-FILE_IO t = MkEff t FileIO+-- --------------------------------------------------------------------- [ API ] --- ------------------------------------------------------------ [ The Bindings ]------ Bind the IO context handlers to functions. These functions will run--- in the IO context.---+-- -------------------------------------------------------- [ Open/Close/Query ] -||| Open a file with the specified mode.+||| Open a file. |||-||| @ fname The file name to be opened.-||| @ m The file mode.+||| @ fname the filename.+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,+||| ReadWriteTruncate, or ReadAppend+||| open : (fname : String)- -> (m : Mode)- -> Eff Bool [FILE_IO ()]- (\res => [FILE_IO (case res of- True => OpenFile m- False => ())])+ -> (m : Mode)+ -> Eff (FileOpSuccess)+ [FILE ()]+ (\res => [FILE (calcResourceTy m res)]) open f m = call $ Open f m +||| Open a file using C11 extended modes.+|||+||| @ fname the filename+||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite,+||| ReadWriteTruncate, or ReadAppend+openX : (fname : String)+ -> (m : Mode)+ -> Eff (FileOpSuccess)+ [FILE ()]+ (\res => [FILE (calcResourceTy m res)])+openX f m = call $ OpenX f m ||| Close a file.-close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]-close = call $ Close+close : Eff () [FILE (FileHandle m)] [FILE ()]+close = call (Close) -||| Read a line from the file.-readLine : Eff String [FILE_IO (OpenFile Read)]-readLine = call $ ReadLine+||| Have we reached the end of the file.+eof : {auto prf : ValidModeRead m}+ -> Eff Bool [FILE (FileHandle m)]+eof = call FEOF -||| Write a string to a file.-writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]-writeString str = call $ WriteString str+flush : Eff () [FILE (FileHandle m)]+flush = call FFlush -||| Write a line to a file.-writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]-writeLine str = call $ WriteString (str ++ "\n")+-- -------------------------------------------------------------------- [ Read ] -||| End of file?-eof : Eff Bool [FILE_IO (OpenFile Read)]-eof = call $ EOF+||| Read a `Char`.+readChar : {auto prf : ValidModeRead m}+ -> Eff (FileOpResult Char)+ [FILE (FileHandle m)]+readChar = call FGetC -||| Read a complete file, returning a user defined error if-||| unsuccesful.-|||-readFile : (errFunc : String -> e)- -> (fname : String)- -> Eff (Either e String) [FILE_IO ()]-readFile errFunc fname = do- case !(open fname Read) of- False => pure $ Left (errFunc fname)- True => do- src <- readAcc ""- close- pure $ Right src- where- readAcc : String -> Eff String [FILE_IO (OpenFile Read)]- readAcc acc = if (not !(eof))- then readAcc (acc ++ !(readLine))- else pure acc+||| Read a complete line.+readLine : {auto prf : ValidModeRead m}+ -> Eff (FileOpResult String)+ [FILE (FileHandle m)]+readLine = call FGetLine -||| Write a file containing the provided string, returning a user-||| defined error if unsuccesful.-|||-writeFile : (errFunc : String -> e)- -> (fname : String)- -> (content : String)- -> Eff (Either e ()) [FILE_IO ()]-writeFile errFunc fname content = do- case !(open fname WriteTruncate) of- True => do- writeString content- close- pure $ Right ()- False => pure $ Left (errFunc fname)+-- ------------------------------------------------------------------- [ Write ] +||| Write a string to the file.+writeString : (str : String)+ -> {auto prf : ValidModeWrite m}+ -> Eff (FileOpSuccess)+ [FILE (FileHandle m)]+writeString str = call $ FPutStr str -namespace Default- readFile : String -> Eff (Either String String) [FILE_IO ()]- readFile = File.readFile id+||| Write a complete line to the file.+writeLine : (str : String)+ -> {auto prf : ValidModeWrite m}+ -> Eff (FileOpSuccess)+ [FILE (FileHandle m)]+writeLine str = call $ FPutStrLn str - writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]- writeFile = File.writeFile id+-- -------------------------------------------------------------- [ Whole File ]++||| Read the contents of a file into a string.+|||+||| This checks the size of+||| the file before beginning to read, and only reads that many bytes,+||| to ensure that it remains a total function if the file is appended+||| to while being read.+|||+||| Returns an error if fname is not a normal file.+readFile : (fname : String)+ -> Eff (FileOpResult String)+ [FILE ()]+readFile fn = call $ FReadFile fn++||| Create a file and write contents to the file.+writeFile : (fname : String)+ -> (contents : String)+ -> Eff (FileOpSuccess)+ [FILE ()]+writeFile fn str = call $ FWriteFile fn str+ -- --------------------------------------------------------------------- [ EOF ]
libs/prelude/Builtins.idr view
@@ -12,7 +12,7 @@ namespace Builtins ||| The non-dependent pair type, also known as conjunction. ||| @A the type of the left elements in the pair- ||| @B the type of the left elements in the pair+ ||| @B the type of the right elements in the pair %elim data Pair : (A : Type) -> (B : Type) -> Type where ||| A pair of elements ||| @a the left element of the pair@@ -26,7 +26,7 @@ ||| The non-dependent pair type, also known as conjunction, usable with ||| UniqueTypes. ||| @A the type of the left elements in the pair- ||| @B the type of the left elements in the pair+ ||| @B the type of the right elements in the pair data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where ||| A pair of elements ||| @a the left element of the pair@@ -73,7 +73,6 @@ ||| For 'symbol syntax. 'foo becomes Symbol_ "foo" data Symbol_ : String -> Type where- infix 5 ~=~
libs/prelude/Prelude/Traversable.idr view
@@ -9,20 +9,28 @@ %access public export +||| Map each element of a structure to a computation, evaluate those+||| computations and discard the results. traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f () traverse_ f = foldr ((*>) . f) (pure ()) +||| Evaluate each computation in a structure and discard the results sequence_ : (Foldable t, Applicative f) => t (f a) -> f () sequence_ = foldr (*>) (pure ()) +||| Like `traverse_` but with the arguments flipped for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f () for_ = flip traverse_ interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where+ ||| Map each element of a structure to a computation, evaluate those+ ||| computations and combine the results. traverse : Applicative f => (a -> f b) -> t a -> f (t b) +||| Evaluate each computation in a structure and collect the results sequence : (Traversable t, Applicative f) => t (f a) -> f (t a) sequence = traverse id +||| Like `traverse` but with the arguments flipped for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b) for = flip traverse
rts/idris_rts.c view
@@ -792,6 +792,9 @@ case CT_MANAGEDPTR: cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size); break;+ case CT_CDATA:+ cl = MKCDATAc(vm, x->info.c_heap_item);+ break; case CT_BITS8: cl = idris_b8CopyForGC(vm, x); break;
src/IRTS/CodegenCommon.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DeriveGeneric #-} {-| Module : IRTS.CodegenCommon Description : Common data structures required for all code generators.@@ -7,12 +8,14 @@ -} module IRTS.CodegenCommon where +import GHC.Generics (Generic)+ import Idris.Core.TT import IRTS.Simplified import IRTS.Defunctionalise data DbgLevel = NONE | DEBUG | TRACE deriving Eq-data OutputType = Raw | Object | Executable deriving (Eq, Show)+data OutputType = Raw | Object | Executable deriving (Eq, Show, Generic) -- | Everything which might be needed in a code generator. --
src/IRTS/CodegenJavaScript.hs view
@@ -17,6 +17,7 @@ import Idris.AbsSyntax hiding (TypeCase) import IRTS.Bytecode import IRTS.Lang+import IRTS.Exports import IRTS.Simplified import IRTS.Defunctionalise import IRTS.CodegenCommon@@ -103,12 +104,12 @@ codegenJavaScript :: CodeGenerator codegenJavaScript ci = codegenJS_all JavaScript (simpleDecls ci)- (includes ci) [] (outputFile ci) (outputType ci)+ (includes ci) [] (outputFile ci) (exportDecls ci) (outputType ci) codegenNode :: CodeGenerator codegenNode ci = codegenJS_all Node (simpleDecls ci)- (includes ci) (compileLibs ci) (outputFile ci) (outputType ci)+ (includes ci) (compileLibs ci) (outputFile ci) (exportDecls ci) (outputType ci) codegenJS_all :: JSTarget@@ -116,14 +117,16 @@ -> [FilePath] -> [String] -> FilePath+ -> [ExportIFace] -> OutputType -> IO ()-codegenJS_all target definitions includes libs filename outputType = do+codegenJS_all target definitions includes libs filename exports outputType = do let bytecode = map toBC definitions let info = initCompileInfo bytecode let js = concatMap (translateDecl info) bytecode let full = concatMap processFunction js- let code = deadCodeElim full+ let exportedNames = map translateName ((getExpNames exports) ++ [sUN "call__IO"])+ let code = deadCodeElim exportedNames full let ext = takeExtension filename let isHtml = target == JavaScript && ext == ".html" let htmlPrologue = T.pack "<!doctype html><html><head><script>\n"@@ -150,6 +153,7 @@ let jsSource = T.pack runtime `T.append` T.concat (map compileJS opt) `T.append` T.concat (map compileJS cons)+ `T.append` T.concat (map compileJS (map genInterface (concatMap getExps exports))) `T.append` main `T.append` invokeMain let source = if isHtml@@ -161,14 +165,17 @@ , writable = True }) where- deadCodeElim :: [JS] -> [JS]- deadCodeElim js = concatMap collectFunctions js+ deadCodeElim :: [String] -> [JS] -> [JS]+ deadCodeElim exports js = concatMap (collectFunctions exports) js where- collectFunctions :: JS -> [JS]- collectFunctions fun@(JSAlloc name _)+ collectFunctions :: [String] -> JS -> [JS]+ collectFunctions _ fun@(JSAlloc name _) | name == translateName (sMN 0 "runMain") = [fun] - collectFunctions fun@(JSAlloc name (Just (JSFunction _ body))) =+ collectFunctions exports fun@(JSAlloc name _)+ | name `elem` exports = [fun]++ collectFunctions _ fun@(JSAlloc name (Just (JSFunction _ body))) = let invokations = sum $ map ( \x -> execState (countInvokations name x) 0 ) js@@ -273,6 +280,7 @@ invokeMain :: T.Text invokeMain = compileJS $ JSApp (JSIdent "main") []+ getExps (Export _ _ exp) = exp optimizeConstructors :: [JS] -> ([JS], [JS]) optimizeConstructors js =@@ -1236,6 +1244,33 @@ jsPOP :: JS jsPOP = JSApp (JSProj jsCALLSTACK "pop") []++genInterface :: Export -> JS+genInterface (ExportData name) = JSNoop+genInterface (ExportFun name (FStr jsName) ret args) = JSAlloc jsName+ (Just (JSFunction [] (JSSeq $+ jsFUNPRELUDE +++ pushArgs nargs +++ [jsSTOREOLD d,+ jsBASETOP d 0,+ jsADDTOP d nargs,+ jsCALL d name] +++ retval ret)))+ where+ nargs = length args+ d = CompileInfo [] [] False+ pushArg n = JSAssign (jsTOP n) (JSIndex (JSIdent "arguments") (JSNum (JSInt n)))+ pushArgs 0 = []+ pushArgs n = (pushArg (n-1)):pushArgs (n-1)+ retval (FIO t) = [JSApp (JSIdent "i$RUN") [],+ JSAssign (jsTOP 0) JSNull,+ JSAssign (jsTOP 1) JSNull,+ JSAssign (jsTOP 2) (translateReg RVal),+ jsSTOREOLD d,+ jsBASETOP d 0,+ jsADDTOP d 3,+ jsCALL d (sUN "call__IO")] ++ retval t+ retval t = [JSApp (JSIdent "i$RUN") [], JSReturn (translateReg RVal)] translateBC :: CompileInfo -> BC -> JS translateBC info bc
src/IRTS/Compiler.hs view
@@ -529,8 +529,8 @@ -- Transform matching on Delay to applications of Force. irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc]) | delay == txt "Delay"- = do sc' <- irSC top vs $ mkForce n' n sc- return $ LLet n' (LForce (LV (Glob n))) sc'+ = do sc' <- irSC top vs sc -- mkForce n' n sc+ return $ lsubst n' (LForce (LV (Glob n))) sc' -- There are two transformations in this case: --
src/IRTS/Lang.hs view
@@ -5,7 +5,7 @@ License : BSD3 Maintainer : The Idris Community. -}-{-# LANGUAGE PatternGuards, DeriveFunctor #-}+{-# LANGUAGE PatternGuards, DeriveFunctor, DeriveGeneric #-} module IRTS.Lang where @@ -17,6 +17,7 @@ import Data.List import Debug.Trace+import GHC.Generics (Generic) data Endianness = Native | BE | LE deriving (Show, Eq) @@ -93,7 +94,7 @@ -- core or another machine. 'id' is a valid implementation | LExternal Name | LNoOp- deriving (Show, Eq)+ deriving (Show, Eq, Generic) -- Supported target languages for foreign calls @@ -301,6 +302,30 @@ usedIn env (LForeign _ _ args) = concatMap (usedIn env) (map snd args) usedIn env (LOp f args) = concatMap (usedIn env) args usedIn env _ = []++lsubst :: Name -> LExp -> LExp -> LExp+lsubst n new (LV (Glob x)) | n == x = new+lsubst n new (LApp t e args) = let e' = lsubst n new e+ args' = map (lsubst n new) args in+ LApp t e' args'+lsubst n new (LLazyApp fn args) = let args' = map (lsubst n new) args in+ LLazyApp fn args'+lsubst n new (LLazyExp e) = LLazyExp (lsubst n new e)+lsubst n new (LForce e) = LForce (lsubst n new e)+lsubst n new (LLet v val sc) = LLet v (lsubst n new val) (lsubst n new sc)+lsubst n new (LLam ns sc) = LLam ns (lsubst n new sc)+lsubst n new (LProj e i) = LProj (lsubst n new e) i+lsubst n new (LCon lv t cn args) = let args' = map (lsubst n new) args in+ LCon lv t cn args'+lsubst n new (LOp op args) = let args' = map (lsubst n new) args in+ LOp op args'+lsubst n new (LForeign fd rd args) + = let args' = map (\(d, a) -> (d, lsubst n new a)) args in+ LForeign fd rd args'+lsubst n new (LCase t e alts) = let e' = lsubst n new e+ alts' = map (fmap (lsubst n new)) alts in+ LCase t e' alts'+lsubst n new tm = tm instance Show LExp where show e = show' [] "" e where
src/Idris/AbsSyntaxTree.hs view
@@ -6,7 +6,8 @@ Maintainer : The Idris Community. -} {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,- DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}+ DeriveDataTypeable, DeriveGeneric, TypeSynonymInstances,+ PatternGuards #-} module Idris.AbsSyntaxTree where @@ -47,6 +48,7 @@ import Data.Traversable (Traversable) import Data.Typeable import Data.Foldable (Foldable)+import GHC.Generics (Generic) import Debug.Trace @@ -112,7 +114,7 @@ , opt_evaltypes :: Bool -- ^ normalise types in `:t` , opt_desugarnats :: Bool , opt_autoimpls :: Bool- } deriving (Show, Eq)+ } deriving (Show, Eq, Generic) defaultOpts = IOption { opt_logLevel = 0 , opt_logcats = []@@ -150,7 +152,7 @@ } deriving (Show) data Optimisation = PETransform -- ^ partial eval and associated transforms- deriving (Show, Eq)+ deriving (Show, Eq, Generic) defaultOptimise = [PETransform] @@ -185,7 +187,8 @@ ppOptionIst :: IState -> PPOption ppOptionIst = ppOption . idris_options -data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)+data LanguageExt = TypeProviders | ErrorReflection+ deriving (Show, Eq, Read, Ord, Generic) -- | The output mode in use data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle@@ -196,13 +199,13 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken | ColsWide Int -- ^ Manually specified - must be positive | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise- deriving (Show, Eq)+ deriving (Show, Eq, Generic) -- | If a function has no totality annotation, what do we assume? data DefaultTotality = DefaultCheckingTotal -- ^ Total | DefaultCheckingPartial -- ^ Partial | DefaultCheckingCovering -- ^Total coverage, but may diverge- deriving (Show, Eq)+ deriving (Show, Eq, Generic) -- | The global state used in the Idris monad data IState = IState {@@ -305,13 +308,14 @@ , idris_ttstats :: M.Map Term (Int, Term) , idris_fragile :: Ctxt String -- ^ Fragile names and explanation. }+ deriving Generic -- Required for parsers library, and therefore trifecta instance Show IState where show = const "{internal state}" data SizeChange = Smaller | Same | Bigger | Unknown- deriving (Show, Eq)+ deriving (Show, Eq, Generic) {-! deriving instance Binary SizeChange deriving instance NFData SizeChange@@ -324,7 +328,7 @@ calls :: [Name] , scg :: [SCGEntry] , usedpos :: [(Int, [UsageReason])]- } deriving Show+ } deriving (Show, Generic) {-! deriving instance Binary CGInfo deriving instance NFData CGInfo@@ -384,7 +388,7 @@ | IBCDeprecate Name String | IBCFragile Name String | IBCConstraint FC UConstraint- deriving Show+ deriving (Show, Generic) -- | The initial state for the compiler idrisInit :: IState@@ -420,12 +424,12 @@ data Codegen = Via IRFormat String | Bytecode- deriving (Show, Eq)+ deriving (Show, Eq, Generic) {-! deriving instance NFData Codegen !-} -data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic) data HowMuchDocs = FullDocs | OverviewDocs @@ -511,7 +515,7 @@ | IErasure | ICoverage | IIBC- deriving (Show, Eq, Ord)+ deriving (Show, Eq, Ord, Generic) strLogCat :: LogCat -> String strLogCat IParse = "parser"@@ -606,7 +610,7 @@ | DesugarNats | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics- deriving (Show, Eq)+ deriving (Show, Eq, Generic) data ElabShellCmd = EQED | EAbandon@@ -625,7 +629,7 @@ | Infixr { prec :: Int } | InfixN { prec :: Int } | PrefixN { prec :: Int }- deriving Eq+ deriving (Eq, Generic) {-! deriving instance Binary Fixity deriving instance NFData Fixity@@ -638,7 +642,7 @@ show (PrefixN i) = "prefix " ++ show i data FixDecl = Fix Fixity String- deriving Eq+ deriving (Eq, Generic) instance Show FixDecl where show (Fix f s) = show f ++ " " ++ s@@ -653,7 +657,7 @@ data Static = Static | Dynamic- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) {-! deriving instance Binary Static deriving instance NFData Static@@ -677,7 +681,7 @@ , pstatic :: Static , pscript :: PTerm }- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) {-! deriving instance Binary Plicity@@ -721,7 +725,7 @@ | Constructor -- ^ Data constructor type | AutoHint -- ^ use in auto implicit search | PEGenerated -- ^ generated by partial evaluator- deriving (Show, Eq)+ deriving (Show, Eq, Generic) {-! deriving instance Binary FnOpt deriving instance NFData FnOpt@@ -739,7 +743,7 @@ -- | Type provider - what to provide data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term | ProvPostulate t -- ^ goal type must be Type, so only term- deriving (Show, Eq, Functor)+ deriving (Show, Eq, Functor, Generic) type ProvideWhat = ProvideWhat' PTerm @@ -824,7 +828,7 @@ -- | FC is decl-level, for errors, and Strings represent the -- namespace | PRunElabDecl FC t [String]- deriving Functor+ deriving (Functor, Generic) {-! deriving instance Binary PDecl' deriving instance NFData PDecl'@@ -851,6 +855,7 @@ | DFragile Name String | DAutoImplicits Bool | DUsed FC Name Name+ deriving Generic -- | A set of instructions for things that need to happen in IState -- after a term elaboration when there's been reflected elaboration.@@ -895,7 +900,7 @@ | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t] | PClauseR FC [t] t [PDecl' t] | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]- deriving Functor+ deriving (Functor, Generic) {-! deriving instance Binary PClause' deriving instance NFData PClause'@@ -913,7 +918,7 @@ | PLaterdecl { d_name :: Name , d_name_fc :: FC , d_tcon :: t- } deriving Functor+ } deriving (Functor, Generic) -- | Transform the FCs in a PData and its associated terms. The first -- function transforms the general-purpose FCs, and the second@@ -1103,7 +1108,7 @@ data PunInfo = IsType | IsTerm | TypeOrTerm- deriving (Eq, Show, Data, Typeable)+ deriving (Eq, Show, Data, Typeable, Generic) -- | High level language terms data PTerm = PQuote Raw -- ^ Inclusion of a core term into the@@ -1170,12 +1175,12 @@ | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source -- location that will be used to highlight it later.- deriving (Eq, Data, Typeable)+ deriving (Eq, Data, Typeable, Generic) data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed | FirstSuccess | TryImplicit- deriving (Eq, Data, Typeable)+ deriving (Eq, Data, Generic, Typeable) -- | Transform the FCs in a PTerm. The first function transforms the -- general-purpose FCs, and the second transforms those that are used@@ -1296,7 +1301,7 @@ | TFail [ErrorReportPart] | Qed | Abandon | SourceFC- deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)+ deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable) {-! deriving instance Binary PTactic' deriving instance NFData PTactic'@@ -1343,7 +1348,7 @@ | DoBindP FC t t [(t,t)] | DoLet FC Name FC t t -- ^ second FC is precise name location | DoLetP FC t t- deriving (Eq, Functor, Data, Typeable)+ deriving (Eq, Functor, Data, Generic, Typeable) {-! deriving instance Binary PDo' deriving instance NFData PDo'@@ -1384,13 +1389,13 @@ , getScript :: t , getTm :: t }- deriving (Show, Eq, Functor, Data, Typeable)+ deriving (Show, Eq, Functor, Data, Generic, Typeable) data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) instance Sized a => Sized (PArg' a) where size (PImp p _ l nm trm) = 1 + size nm + size trm@@ -1480,7 +1485,7 @@ , class_params :: [Name] , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded , class_determiners :: [Int]- } deriving Show+ } deriving (Show, Generic) {-! deriving instance Binary ClassInfo deriving instance NFData ClassInfo@@ -1491,17 +1496,17 @@ record_parameters :: [(Name,PTerm)] , record_constructor :: Name , record_projections :: [Name]- } deriving Show+ } deriving (Show, Generic) -- Type inference data data TIData = TIPartial -- ^ a function with a partially defined type | TISolution [Term] -- ^ possible solutions to a metavariable in a type- deriving Show+ deriving (Show, Generic) -- | Miscellaneous information about functions data FnInfo = FnInfo { fn_params :: [Int] }- deriving Show+ deriving (Show, Generic) {-! deriving instance Binary FnInfo deriving instance NFData FnInfo@@ -1510,7 +1515,7 @@ data OptInfo = Optimise { inaccessible :: [(Int,Name)] -- includes names for error reporting , detaggable :: Bool- } deriving Show+ } deriving (Show, Generic) {-! deriving instance Binary OptInfo deriving instance NFData OptInfo@@ -1528,7 +1533,7 @@ , dsl_lambda :: Maybe t , dsl_let :: Maybe t , dsl_pi :: Maybe t- } deriving (Show, Functor)+ } deriving (Show, Functor, Generic) {-! deriving instance Binary DSL' deriving instance NFData DSL'@@ -1539,7 +1544,7 @@ data SynContext = PatternSyntax | TermSyntax | AnySyntax- deriving Show+ deriving (Show, Generic) {-! deriving instance Binary SynContext deriving instance NFData SynContext@@ -1547,7 +1552,7 @@ data Syntax = Rule [SSymbol] PTerm SynContext | DeclRule [SSymbol] [PDecl]- deriving Show+ deriving (Show, Generic) syntaxNames :: Syntax -> [Name] syntaxNames (Rule syms _ _) = mapMaybe ename syms@@ -1570,7 +1575,7 @@ | Binding Name | Expr Name | SimpleExpr Name- deriving (Show, Eq)+ deriving (Show, Eq, Generic) {-!@@ -1579,6 +1584,7 @@ !-} newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }+ deriving Generic emptySyntaxRules :: SyntaxRules emptySyntaxRules = SyntaxRules []@@ -1632,7 +1638,7 @@ data Using = UImplicit Name PTerm | UConstraint Name [Name]- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) {-! deriving instance Binary Using deriving instance NFData Using@@ -1656,7 +1662,7 @@ , syn_in_quasiquote :: Int , syn_toplevel :: Bool , withAppAllowed :: Bool- } deriving Show+ } deriving (Show, Generic) {-! deriving instance NFData SyntaxInfo deriving instance Binary SyntaxInfo
src/Idris/CaseSplit.hs view
@@ -75,7 +75,7 @@ logElab 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats) -- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty)) -- iputStrLn (show pats)- let t = mergeUserImpl (addImplPat ist t') (delab ist tm)+ let t = mergeUserImpl (addImplPat ist t') (delabDirect ist tm) let ctxt = tt_ctxt ist case lookup n pats of Nothing -> ifail $ show n ++ " is not a pattern variable"@@ -247,7 +247,7 @@ elabNewPat :: PTerm -> Idris (Bool, PTerm) elabNewPat t = idrisCatch (do (tm, ty) <- elabVal (recinfo (fileFC "casesplit")) ELHS t i <- getIState- return (True, delab i tm))+ return (True, delabDirect i tm)) (\e -> do i <- getIState logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n" ++ pshow i e
src/Idris/Colours.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE DeriveGeneric #-} {-| Module : Idris.Colours Description : Support for colours within Idris.@@ -14,6 +15,7 @@ , colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise ) where +import GHC.Generics (Generic) import System.Console.ANSI import System.IO (Handle) @@ -37,7 +39,7 @@ , promptColour :: IdrisColour , postulateColour :: IdrisColour }- deriving (Eq, Show)+ deriving (Eq, Show, Generic) -- | Idris's default console colour theme defaultTheme :: ColourTheme
src/Idris/Core/CaseTree.hs view
@@ -18,7 +18,8 @@ in order to allow for better optimisation opportunities. -}-{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}+{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances,+ DeriveGeneric #-} module Idris.Core.CaseTree ( CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo@@ -36,6 +37,7 @@ import Data.List hiding (partition) import qualified Data.List(partition) import Debug.Trace+import GHC.Generics (Generic) data CaseDef = CaseDef [Name] !SC [Term] deriving Show@@ -45,14 +47,14 @@ | STerm !t | UnmatchedCase String -- ^ error message | ImpossibleCase -- ^ already checked to be impossible- deriving (Eq, Ord, Functor)+ deriving (Eq, Ord, Functor, Generic) {-! deriving instance Binary SC' deriving instance NFData SC' !-} data CaseType = Updatable | Shared- deriving (Eq, Ord, Show)+ deriving (Eq, Ord, Show, Generic) type SC = SC' Term @@ -61,7 +63,7 @@ | ConstCase Const !(SC' t) | SucCase Name !(SC' t) | DefaultCase !(SC' t)- deriving (Show, Eq, Ord, Functor)+ deriving (Show, Eq, Ord, Functor, Generic) {-! deriving instance Binary CaseAlt' deriving instance NFData CaseAlt'@@ -249,7 +251,8 @@ -- Work Right to Left simpleCase :: Bool -> SC -> Bool ->- Phase -> FC -> [Int] -> [Type] ->+ Phase -> FC -> [Int] -> + [(Type, Bool)] -> -- (Argument type, whether it's canonical) [([Name], Term, Term)] -> ErasureInfo -> TC CaseDef@@ -271,7 +274,7 @@ OK pats -> let numargs = length (fst (head pats)) ns = take numargs args- (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats+ (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys) (tree, st) = runCaseBuilder erInfo (match ns' ps' defcase) ([], numargs, [])@@ -429,28 +432,38 @@ -- -- The first argument means [(Name, IsInaccessible)]. -order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])-order [] cs = ([], cs)-order ns' [] = (map fst ns', [])-order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))- -- only sort the arguments where there is no clash in- -- constructor tags between families, and no constructor/constant- -- clash, because otherwise we can't reliable make the- -- case distinction on evaluation- (patnames_ord, patnames_rest)- = Data.List.partition (noClash . map snd) patnames- -- note: sortBy . reverse is not nonsense because sortBy is stable- pats' = transpose (sortBy moreDistinct (reverse patnames_ord)- ++ patnames_rest) in- (getNOrder pats', zipWith rebuild pats' cs)+order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])+-- do nothing at compile time: FIXME (EB): Put this in after checking +-- implications for Franck's reflection work... see issue 3233+-- order CompileTime ns cs _ = (map fst ns, cs) +order _ [] cs cans = ([], cs)+order _ ns' [] cans = (map fst ns', [])+order phase ns' cs cans + = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))+ -- only sort the arguments where there is no clash in+ -- constructor tags between families, the argument type is canonical,+ -- and no constructor/constant+ -- clash, because otherwise we can't reliable make the+ -- case distinction on evaluation+ (patnames_ord, patnames_rest)+ = Data.List.partition (noClash . map snd) patnames + patnames_ord' = case phase of+ CompileTime -> patnames_ord+ -- reversing tends to make better case trees+ -- and helps erasure+ RunTime -> reverse patnames_ord+ pats' = transpose (sortBy moreDistinct patnames_ord'+ ++ patnames_rest) in+ (getNOrder pats', zipWith rebuild pats' cs) where getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs) getNOrder (c : _) = map (fst . fst) c - rebuild patnames clause = (map snd patnames, snd clause)+ rebuild patnames clause = (map (snd . snd) patnames, snd clause) noClash [] = True- noClash (p : ps) = not (any (clashPat p) ps) && noClash ps+ noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps)) + && noClash ps clashPat (PCon _ _ _ _) (PConst _) = True clashPat (PConst _) (PCon _ _ _ _) = True@@ -460,12 +473,13 @@ clashPat _ _ = False -- this compares (+isInaccessible, -numberOfCases)- moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))- (snd . fst . head $ ys, numNames [] (map snd xs))+ moreDistinct xs ys + = compare (snd . fst . head $ xs, numNames [] (map snd ys))+ (snd . fst . head $ ys, numNames [] (map snd xs)) - numNames xs (PCon _ n _ _ : ps)+ numNames xs ((_, PCon _ n _ _) : ps) | not (Left n `elem` xs) = numNames (Left n : xs) ps- numNames xs (PConst c : ps)+ numNames xs ((_, PConst c) : ps) | not (Right c `elem` xs) = numNames (Right c : xs) ps numNames xs (_ : ps) = numNames xs ps numNames xs [] = length xs
src/Idris/Core/DeepSeq.hs view
@@ -1,6 +1,6 @@ {-| Module : Idris.Core.DeepSeq-Description : Marshalling information for TT.+Description : NFData instances for TT. Copyright : License : BSD3 Maintainer : The Idris Community.@@ -16,287 +16,46 @@ import Control.DeepSeq -instance NFData Name where- rnf (UN x1) = rnf x1 `seq` ()- rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (SN x1) = rnf x1 `seq` ()- rnf (SymRef x1) = rnf x1 `seq` ()+instance NFData Name -instance NFData Context where- rnf ctxt = rnf (next_tvar ctxt) `seq` rnf (definitions ctxt) `seq` ()+instance NFData Context -- | Forcing the contents of a context, for diagnosing and working -- around space leaks forceDefCtxt :: Context -> Context forceDefCtxt (force -> !ctxt) = ctxt -instance NFData NameOutput where- rnf TypeOutput = ()- rnf FunOutput = ()- rnf DataOutput = ()- rnf MetavarOutput = ()- rnf PostulateOutput = ()--instance NFData TextFormatting where- rnf BoldText = ()- rnf ItalicText = ()- rnf UnderlineText = ()--instance NFData Ordering where- rnf LT = ()- rnf EQ = ()- rnf GT = ()--instance NFData OutputAnnotation where- rnf (AnnName x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (AnnBoundName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (AnnConst x1) = rnf x1 `seq` ()- rnf (AnnData x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (AnnType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (AnnKeyword) = ()- rnf (AnnFC x) = rnf x `seq` ()- rnf (AnnTextFmt x) = rnf x `seq` ()- rnf (AnnLink x) = rnf x `seq` ()- rnf (AnnTerm x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (AnnSearchResult x1) = rnf x1 `seq` ()- rnf (AnnErr x1) = rnf x1 `seq` ()- rnf (AnnNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (AnnQuasiquote) = ()- rnf (AnnAntiquote) = ()--instance NFData SpecialName where- rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (MethodN x1) = rnf x1 `seq` ()- rnf (CaseN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ElimN x1) = rnf x1 `seq` ()- rnf (InstanceCtorN x1) = rnf x1 `seq` ()- rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData Universe where- rnf NullType = ()- rnf UniqueType = ()- rnf AllTypes = ()--instance NFData Raw where- rnf (Var x1) = rnf x1 `seq` ()- rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf RType = ()- rnf (RUType x1) = rnf x1 `seq` ()- rnf (RConstant x1) = x1 `seq` ()--instance NFData FC where- rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf NoFC = ()- rnf (FileFC f) = rnf f `seq` ()--instance NFData FC' where- rnf (FC' fc) = rnf fc `seq` ()--instance NFData Provenance where- rnf ExpectedType = ()- rnf InferredVal = ()- rnf GivenVal = ()- rnf (SourceTerm x1) = rnf x1 `seq` ()- rnf (TooManyArgs x1) = rnf x1 `seq` ()--instance NFData UConstraint where- rnf (ULT x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ULE x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData ConstraintFC where- rnf (ConstraintFC x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData Err where- rnf (Msg x1) = rnf x1 `seq` ()- rnf (InternalMsg x1) = rnf x1 `seq` ()- rnf (CantUnify x1 x2 x3 x4 x5 x6)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()- rnf (InfiniteUnify x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (CantConvert x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (UnifyScope x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (ElaboratingArg x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (CantInferType x1) = rnf x1 `seq` ()- rnf (CantMatch x1) = rnf x1 `seq` ()- rnf (ReflectionError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (UniqueKindError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (NotEquality x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (CantIntroduce x1) = rnf x1 `seq` ()- rnf (TooManyArguments x1) = rnf x1 `seq` ()- rnf (WithFnType x1) = rnf x1 `seq` ()- rnf (NoSuchVariable x1) = rnf x1 `seq` ()- rnf (NoTypeDecl x1) = rnf x1 `seq` ()- rnf (NotInjective x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (CantResolve x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (CantResolveAlts x1) = rnf x1 `seq` ()- rnf (NoValidAlts x1) = rnf x1 `seq` ()- rnf (IncompleteTerm x1) = rnf x1 `seq` ()- rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf ProgramLineComment = ()- rnf (Inaccessible x1) = rnf x1 `seq` ()- rnf (UnknownImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()- rnf (AlreadyDefined x1) = rnf x1 `seq` ()- rnf (ProofSearchFail x1) = rnf x1 `seq` ()- rnf (NoRewriting x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (Elaborating x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (ProviderError x1) = rnf x1 `seq` ()- rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (ElabScriptStuck x1) = rnf x1 `seq` ()- rnf (RunningElabScript x1) = rnf x1 `seq` ()- rnf (ElabScriptStaging x1) = rnf x1 `seq` ()- rnf (FancyMsg x1) = rnf x1 `seq` ()--instance NFData ErrorReportPart where- rnf (TextPart x1) = rnf x1 `seq` ()- rnf (TermPart x1) = rnf x1 `seq` ()- rnf (RawPart x1) = rnf x1 `seq` ()- rnf (NamePart x1) = rnf x1 `seq` ()- rnf (SubReport x1) = rnf x1 `seq` ()--instance NFData ImplicitInfo where- rnf (Impl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()--instance (NFData b) => NFData (Binder b) where- rnf (Lam x1) = rnf x1 `seq` ()- rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (Hole x1) = rnf x1 `seq` ()- rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PVar x1) = rnf x1 `seq` ()- rnf (PVTy x1) = rnf x1 `seq` ()--instance NFData UExp where- rnf (UVar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (UVal x1) = rnf x1 `seq` ()--instance NFData NameType where- rnf Bound = ()- rnf Ref = ()- rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData NativeTy where- rnf IT8 = ()- rnf IT16 = ()- rnf IT32 = ()- rnf IT64 = ()--instance NFData IntTy where- rnf (ITFixed x1) = rnf x1 `seq` ()- rnf ITNative = ()- rnf ITBig = ()- rnf ITChar = ()--instance NFData ArithTy where- rnf (ATInt x1) = rnf x1 `seq` ()- rnf ATFloat = ()--instance NFData Const where- rnf (I x1) = rnf x1 `seq` ()- rnf (BI x1) = rnf x1 `seq` ()- rnf (Fl x1) = rnf x1 `seq` ()- rnf (Ch x1) = rnf x1 `seq` ()- rnf (Str x1) = rnf x1 `seq` ()- rnf (B8 x1) = rnf x1 `seq` ()- rnf (B16 x1) = rnf x1 `seq` ()- rnf (B32 x1) = rnf x1 `seq` ()- rnf (B64 x1) = rnf x1 `seq` ()- rnf (AType x1) = rnf x1 `seq` ()- rnf WorldType = ()- rnf TheWorld = ()- rnf StrType = ()- rnf VoidType = ()- rnf Forgot = ()--instance (NFData n) => NFData (TT n) where- rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (V x1) = rnf x1 `seq` ()- rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (App x1 x2 x3) = rnf x2 `seq` rnf x3 `seq` ()- rnf (Constant x1) = rnf x1 `seq` ()- rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf Erased = ()- rnf Impossible = ()- rnf (TType x1) = rnf x1 `seq` ()- rnf (UType _) = ()--instance NFData Accessibility where- rnf Public = ()- rnf Frozen = ()- rnf Hidden = ()- rnf Private = ()---instance NFData Totality where- rnf (Total x1) = rnf x1 `seq` ()- rnf Productive = ()- rnf (Partial x1) = rnf x1 `seq` ()- rnf Unchecked = ()- rnf Generated = ()--instance NFData PReason where- rnf (Other x1) = rnf x1 `seq` ()- rnf Itself = ()- rnf NotCovering = ()- rnf NotPositive = ()- rnf (UseUndef x1) = rnf x1 `seq` ()- rnf ExternalIO = ()- rnf BelieveMe = ()- rnf (Mutual x1) = rnf x1 `seq` ()- rnf NotProductive = ()--instance NFData MetaInformation where- rnf EmptyMI = ()- rnf (DataMI x1) = rnf x1 `seq` ()--instance NFData Def where- rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (CaseOp x1 x2 x3 x4 x5 x6)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()--instance NFData CaseInfo where- rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()--instance NFData CaseDefs where- rnf (CaseDefs x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()--instance (NFData t) => NFData (SC' t) where- rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (STerm x1) = rnf x1 `seq` ()- rnf (UnmatchedCase x1) = rnf x1 `seq` ()- rnf ImpossibleCase = ()--instance (NFData t) => NFData (CaseAlt' t) where- rnf (ConCase x1 x2 x3 x4)- = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()- rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()- rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()- rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()- rnf (DefaultCase x1) = rnf x1 `seq` ()+instance NFData NameOutput+instance NFData TextFormatting+instance NFData Ordering+instance NFData OutputAnnotation+instance NFData SpecialName+instance NFData Universe+instance NFData Raw+instance NFData FC+instance NFData FC'+instance NFData Provenance+instance NFData UConstraint+instance NFData ConstraintFC+instance NFData Err+instance NFData ErrorReportPart+instance NFData ImplicitInfo+instance (NFData b) => NFData (Binder b)+instance NFData UExp+instance NFData NameType+instance NFData NativeTy+instance NFData IntTy+instance NFData ArithTy+instance NFData Const+instance (NFData a) => NFData (AppStatus a)+instance (NFData n) => NFData (TT n)+instance NFData Accessibility+instance NFData Totality+instance NFData PReason+instance NFData MetaInformation+instance NFData Def+instance NFData CaseInfo+instance NFData CaseDefs+instance NFData CaseType+instance (NFData t) => NFData (SC' t)+instance (NFData t) => NFData (CaseAlt' t)
src/Idris/Core/Evaluate.hs view
@@ -6,7 +6,7 @@ Maintainer : The Idris Community. -} {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,- PatternGuards #-}+ PatternGuards, DeriveGeneric #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,@@ -21,7 +21,8 @@ lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal, mapDefCtxt, lookupTotal, lookupTotalExact, lookupInjectiveExact,- lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,+ lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, + isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName, Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions, isUniverse) where @@ -31,6 +32,7 @@ import qualified Data.Binary as B import Data.Binary hiding (get, put) import Data.Maybe (listToMaybe)+import GHC.Generics (Generic) import Idris.Core.TT import Idris.Core.CaseTree@@ -696,10 +698,11 @@ | Operator Type Int ([Value] -> Maybe Value) | CaseOp CaseInfo !Type- ![Type] -- argument types+ ![(Type, Bool)] -- argument types, whether canonical ![Either Term (Term, Term)] -- original definition ![([Name], Term, Term)] -- simplified for totality check definition !CaseDefs+ deriving Generic -- [Name] SC -- Compile time case definition -- [Name] SC -- Run time cae definitions @@ -709,12 +712,14 @@ cases_inlined :: !([Name], SC), cases_runtime :: !([Name], SC) }+ deriving Generic data CaseInfo = CaseInfo { case_inlinable :: Bool, -- decided by machine case_alwaysinline :: Bool, -- decided by %inline flag tc_dictionary :: Bool }+ deriving Generic {-! deriving instance Binary Def@@ -761,7 +766,7 @@ -- Private => Programs can't access the name, doesn't reduce internally data Accessibility = Hidden | Public | Frozen | Private- deriving (Eq, Ord)+ deriving (Eq, Ord, Generic) {-! deriving instance NFData Accessibility !-}@@ -780,7 +785,7 @@ | Partial PReason | Unchecked | Generated- deriving Eq+ deriving (Eq, Generic) {-! deriving instance NFData Totality !-}@@ -788,7 +793,7 @@ -- | Reasons why a function may not be total data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name | ExternalIO | BelieveMe | Mutual [Name] | NotProductive- deriving (Show, Eq)+ deriving (Show, Eq, Generic) {-! deriving instance NFData PReason !-}@@ -825,14 +830,14 @@ data MetaInformation = EmptyMI -- ^ No meta-information | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters- deriving (Eq, Show)+ deriving (Eq, Show, Generic) -- | Contexts used for global definitions and for proof state. They contain -- universe constraints and existing definitions. data Context = MkContext { next_tvar :: Int, definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)- } deriving Show+ } deriving (Show, Generic) -- | The initial empty context@@ -911,7 +916,7 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo -> Bool -> SC -> -- default case Bool -> Bool ->- [Type] -> -- argument types+ [(Type, Bool)] -> -- argument types, whether canonical [Int] -> -- inaccessible arguments [Either Term (Term, Term)] -> [([Name], Term, Term)] -> -- totality@@ -1014,6 +1019,15 @@ -- | Get the single type that matches some name precisely lookupTyExact :: Name -> Context -> Maybe Type lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)++-- | Return true if the given type is a concrete type familyor primitive+-- False it it's a function to compute a type or a variable+isCanonical :: Type -> Context -> Bool+isCanonical t ctxt+ = case unApply t of+ (P _ n _, _) -> isConName n ctxt+ (Constant _, _) -> True+ _ -> False isConName :: Name -> Context -> Bool isConName n ctxt = isTConName n ctxt || isDConName n ctxt
src/Idris/Core/ProofState.hs view
@@ -1058,7 +1058,7 @@ (getProofTerm (pterm ps)) }, "") processTactic UnifyProblems ps = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))- pterm' = updateSolved ns' (pterm ps)+ pterm' = orderUpdateSolved ns' (pterm ps) traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $ return (ps { pterm = pterm', solved = Nothing, problems = probs', previous = Just ps, plog = "",@@ -1067,6 +1067,8 @@ dotted = filter (notIn ns') (dotted ps), holes = holes ps \\ (map fst ns') }, plog ps) where notIn ns (h, _) = h `notElem` map fst ns+ orderUpdateSolved [] t = t+ orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t) processTactic (MatchProblems all) ps = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps)) (ns'', probs'') = matchProblems all ps ns' probs'
src/Idris/Core/TT.hs view
@@ -23,7 +23,7 @@ programs with implicit syntax into fully explicit terms. -} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,- DeriveDataTypeable, PatternGuards #-}+ DeriveDataTypeable, DeriveGeneric, PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Core.TT( AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)@@ -80,6 +80,7 @@ import qualified Data.Binary as B import Data.Binary hiding (get, put) import Foreign.Storable (sizeOf)+import GHC.Generics (Generic) import Numeric.IEEE (IEEE (identicalIEEE)) @@ -96,7 +97,7 @@ } | NoFC -- ^ Locations for machine-generated terms | FileFC { _fc_fname :: String } -- ^ Locations with file only- deriving (Data, Typeable, Ord)+ deriving (Data, Generic, Typeable, Ord) -- TODO: find uses and destroy them, doing this case analysis at call sites -- | Give a notion of filename associated with an FC@@ -159,7 +160,7 @@ _ == _ = True -- | FC with equality-newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Typeable, Ord)+newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Generic, Typeable, Ord) instance Eq FC' where FC' fc == FC' fc' = fcEq fc fc'@@ -198,10 +199,10 @@ show (FileFC f) = f -- | Output annotation for pretty-printed name - decides colour-data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq)+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Generic) -- | Text formatting output-data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq)+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Generic) -- | Output annotations for pretty-printing data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)@@ -227,7 +228,7 @@ -- from that file. | AnnQuasiquote | AnnAntiquote- deriving (Show, Eq)+ deriving (Show, Eq, Generic) -- | Used for error reflection data ErrorReportPart = TextPart String@@ -235,7 +236,7 @@ | TermPart Term | RawPart Raw | SubReport [ErrorReportPart]- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) data Provenance = ExpectedType@@ -243,7 +244,7 @@ | InferredVal | GivenVal | SourceTerm Term- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) {-! deriving instance NFData Err deriving instance Binary Err@@ -309,7 +310,7 @@ | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script | ElabScriptStaging Name | FancyMsg [ErrorReportPart]- deriving (Eq, Functor, Data, Typeable)+ deriving (Eq, Functor, Data, Generic, Typeable) type Err = Err' Term @@ -467,7 +468,7 @@ | MN !Int !T.Text -- ^ Machine chosen names | SN !SpecialName -- ^ Decorated function names | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)- deriving (Eq, Ord, Data, Typeable)+ deriving (Eq, Ord, Data, Generic, Typeable) txt :: String -> T.Text txt = T.pack@@ -510,7 +511,7 @@ | ElimN !Name | InstanceCtorN !Name | MetaN !Name !Name- deriving (Eq, Ord, Data, Typeable)+ deriving (Eq, Ord, Data, Generic, Typeable) {-! deriving instance Binary SpecialName deriving instance NFData SpecialName@@ -675,7 +676,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt) data NativeTy = IT8 | IT16 | IT32 | IT64- deriving (Show, Eq, Ord, Enum, Data, Typeable)+ deriving (Show, Eq, Ord, Enum, Data, Generic, Typeable) instance Pretty NativeTy OutputAnnotation where pretty IT8 = text "Bits8"@@ -684,7 +685,7 @@ pretty IT64 = text "Bits64" data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar- deriving (Show, Eq, Ord, Data, Typeable)+ deriving (Show, Eq, Ord, Data, Generic, Typeable) intTyName :: IntTy -> String intTyName ITNative = "Int"@@ -693,7 +694,7 @@ intTyName (ITChar) = "Char" data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723- deriving (Show, Eq, Ord, Data, Typeable)+ deriving (Show, Eq, Ord, Data, Generic, Typeable) {-! deriving instance NFData IntTy deriving instance NFData NativeTy@@ -725,7 +726,7 @@ | AType ArithTy | StrType | WorldType | TheWorld | VoidType | Forgot- deriving (Ord, Data, Typeable)+ deriving (Ord, Data, Generic, Typeable) -- We need to compare Double using bit-pattern identity rather than -- Haskell's Eq, which equates 0.0 and -0.0, leading to a@@ -821,7 +822,7 @@ constDocs prim = "Undocumented" data Universe = NullType | UniqueType | AllTypes- deriving (Eq, Ord, Data, Typeable)+ deriving (Eq, Ord, Data, Generic, Typeable) instance Show Universe where show UniqueType = "UniqueType"@@ -834,7 +835,7 @@ | RType | RUType Universe | RConstant Const- deriving (Show, Eq, Data, Typeable)+ deriving (Show, Eq, Data, Generic, Typeable) instance Sized Raw where size (Var name) = 1@@ -854,7 +855,7 @@ data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool, machine_gen :: Bool }- deriving (Show, Eq, Ord, Data, Typeable)+ deriving (Show, Eq, Ord, Data, Generic, Typeable) {-! deriving instance Binary ImplicitInfo@@ -906,7 +907,7 @@ -- that make up pattern-match clauses) | PVTy { binderTy :: !b } -- ^ The type of a pattern binding- deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable) {-! deriving instance Binary Binder deriving instance NFData Binder@@ -951,7 +952,7 @@ -- | Universe expressions for universe checking data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate | UVal Int -- ^ explicit universe level- deriving (Eq, Ord, Data, Typeable)+ deriving (Eq, Ord, Data, Generic, Typeable) {-! deriving instance NFData UExp !-}@@ -969,11 +970,11 @@ -- | Universe constraints data UConstraint = ULT UExp UExp -- ^ Strictly less than | ULE UExp UExp -- ^ Less than or equal to- deriving (Eq, Ord, Data, Typeable)+ deriving (Eq, Ord, Data, Generic, Typeable) data ConstraintFC = ConstraintFC { uconstraint :: UConstraint, ufc :: FC }- deriving (Show, Data, Typeable)+ deriving (Show, Data, Generic, Typeable) instance Eq ConstraintFC where x == y = uconstraint x == uconstraint y@@ -991,7 +992,7 @@ | Ref | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor- deriving (Show, Ord, Data, Typeable)+ deriving (Show, Ord, Data, Generic, Typeable) {-! deriving instance Binary NameType deriving instance NFData NameType@@ -1013,7 +1014,7 @@ data AppStatus n = Complete | MaybeHoles | Holes [n]- deriving (Eq, Ord, Functor, Data, Typeable, Show)+ deriving (Eq, Ord, Functor, Data, Generic, Typeable, Show) -- | Terms in the core language. The type parameter is the type of -- identifiers used for bindings and explicit named references;@@ -1031,7 +1032,7 @@ | Impossible -- ^ special case for totality checking | TType UExp -- ^ the type of types at some level | UType Universe -- ^ Uniqueness type universe (disjoint from TType)- deriving (Ord, Functor, Data, Typeable)+ deriving (Ord, Functor, Data, Generic, Typeable) {-! deriving instance Binary TT deriving instance NFData TT@@ -1096,7 +1097,7 @@ | DefaultEliminator -- ^ Set if an eliminator should be generated for data type | DefaultCaseFun -- ^ Set if a case function should be generated for data type | DataErrRev- deriving (Show, Eq)+ deriving (Show, Eq, Generic) type DataOpts = [DataOpt] @@ -1105,7 +1106,7 @@ data_opts :: DataOpts, param_pos :: [Int], mutual_types :: [Name] }- deriving Show+ deriving (Show, Generic) {-! deriving instance Binary TypeInfo deriving instance NFData TypeInfo
src/Idris/Coverage.hs view
@@ -557,8 +557,9 @@ findCalls [] Toplevel (dePat rhs') (patvars lhs') (zip pargs [0..]) - findCalls cases Delayed ap@(P _ n _) pvs args- | n == topfn = []+ -- Under a delay, calls are excluded from the graph - if it's a call to a+ -- non-total function we'll find that in the final totality check+ findCalls cases Delayed ap@(P _ n _) pvs args = [] findCalls cases guarded ap@(App _ f a) pvs pargs -- under a call to "assert_total", don't do any checking, just believe -- that it is total.
src/Idris/DeepSeq.hs view
@@ -1,6 +1,6 @@ {-| Module : Idris.DeepSeq-Description : Specify how to marshall Idris' IR.+Description : NFData instances for Idris' types Copyright : License : BSD3 Maintainer : The Idris Community.@@ -26,323 +26,10 @@ import qualified Cheapskate.Types as CT import qualified Idris.Docstrings as D -instance NFData a => NFData (D.Docstring a) where- rnf (D.DocString opts contents) = rnf opts `seq` rnf contents `seq` ()-+-- These types don't have Generic instances instance NFData CT.Options where rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` () -instance NFData ConsoleWidth where- rnf InfinitelyWide = ()- rnf (ColsWide x) = rnf x `seq` ()- rnf AutomaticWidth = ()--instance NFData PrimFn where- rnf (LPlus x) = rnf x `seq` ()- rnf (LMinus x) = rnf x `seq` ()- rnf (LTimes x) = rnf x `seq` ()- rnf (LUDiv x) = rnf x `seq` ()- rnf (LSDiv x) = rnf x `seq` ()- rnf (LURem x) = rnf x `seq` ()- rnf (LSRem x) = rnf x `seq` ()- rnf (LAnd x) = rnf x `seq` ()- rnf (LOr x) = rnf x `seq` ()- rnf (LXOr x) = rnf x `seq` ()- rnf (LCompl x) = rnf x `seq` ()- rnf (LSHL x) = rnf x `seq` ()- rnf (LLSHR x) = rnf x `seq` ()- rnf (LASHR x) = rnf x `seq` ()- rnf (LEq x) = rnf x `seq` ()- rnf (LLt x) = rnf x `seq` ()- rnf (LLe x) = rnf x `seq` ()- rnf (LGt x) = rnf x `seq` ()- rnf (LGe x) = rnf x `seq` ()- rnf (LSLt x) = rnf x `seq` ()- rnf (LSLe x) = rnf x `seq` ()- rnf (LSGt x) = rnf x `seq` ()- rnf (LSGe x) = rnf x `seq` ()- rnf (LSExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (LZExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (LTrunc x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (LStrConcat) = ()- rnf (LStrLt) = ()- rnf (LStrEq) = ()- rnf (LStrLen) = ()- rnf (LIntFloat x) = rnf x `seq` ()- rnf (LFloatInt x) = rnf x `seq` ()- rnf (LIntStr x) = rnf x `seq` ()- rnf (LStrInt x) = rnf x `seq` ()- rnf (LFloatStr) = ()- rnf (LStrFloat) = ()- rnf (LChInt x) = rnf x `seq` ()- rnf (LIntCh x) = rnf x `seq` ()- rnf (LBitCast x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (LFExp) = ()- rnf (LFLog) = ()- rnf (LFSin) = ()- rnf (LFCos) = ()- rnf (LFTan) = ()- rnf (LFASin) = ()- rnf (LFACos) = ()- rnf (LFATan) = ()- rnf (LFSqrt) = ()- rnf (LFFloor) = ()- rnf (LFCeil) = ()- rnf (LFNegate) = ()- rnf (LStrHead) = ()- rnf (LStrTail) = ()- rnf (LStrCons) = ()- rnf (LStrIndex) = ()- rnf (LStrRev) = ()- rnf (LStrSubstr) = ()- rnf (LReadStr) = ()- rnf (LWriteStr) = ()- rnf (LSystemInfo) = ()- rnf (LFork) = ()- rnf (LPar) = ()- rnf (LExternal x) = rnf x `seq` ()- rnf (LNoOp) = ()--instance NFData SyntaxRules where- rnf (SyntaxRules xs) = rnf xs `seq` ()--instance NFData DynamicLib where- rnf (Lib x _) = rnf x `seq` ()---instance NFData Opt where- rnf (Filename str) = rnf str `seq` ()- rnf (Quiet) = ()- rnf (NoBanner) = ()- rnf (ColourREPL bool) = rnf bool `seq` ()- rnf (Idemode) = ()- rnf (IdemodeSocket) = ()- rnf (ShowLoggingCats) = ()- rnf (ShowLibs) = ()- rnf (ShowLibdir) = ()- rnf (ShowIncs) = ()- rnf (ShowPkgs) = ()- rnf (NoBasePkgs) = ()- rnf (NoPrelude) = ()- rnf (NoBuiltins) = ()- rnf (NoREPL) = ()- rnf (OLogging i) = rnf i `seq` ()- rnf (OLogCats cs) = rnf cs `seq` ()- rnf (Output str) = rnf str `seq` ()- rnf (Interface) = ()- rnf (TypeCase) = ()- rnf (TypeInType) = ()- rnf (DefaultTotal) = ()- rnf (DefaultPartial) = ()- rnf (WarnPartial) = ()- rnf (WarnReach) = ()- rnf (EvalTypes) = ()- rnf (DesugarNats) = ()- rnf (NoCoverage) = ()- rnf (ErrContext) = ()- rnf (ShowImpl) = ()- rnf (Verbose) = ()- rnf (Port str) = rnf str `seq` ()- rnf (IBCSubDir str) = rnf str `seq` ()- rnf (ImportDir str) = rnf str `seq` ()- rnf (PkgBuild str) = rnf str `seq` ()- rnf (PkgInstall str) = rnf str `seq` ()- rnf (PkgClean str) = rnf str `seq` ()- rnf (PkgCheck str) = rnf str `seq` ()- rnf (PkgREPL str) = rnf str `seq` ()- rnf (PkgMkDoc str) = rnf str `seq` ()- rnf (PkgTest str) = rnf str `seq` ()- rnf (PkgIndex fp) = rnf fp `seq` ()- rnf (WarnOnly) = ()- rnf (Pkg str) = rnf str `seq` ()- rnf (BCAsm str) = rnf str `seq` ()- rnf (DumpDefun str) = rnf str `seq` ()- rnf (DumpCases str) = rnf str `seq` ()- rnf (UseCodegen cg) = rnf cg `seq` ()- rnf (CodegenArgs str) = rnf str `seq` ()- rnf (OutputTy ot) = rnf ot `seq` ()- rnf (Extension le) = rnf le `seq` ()- rnf (InterpretScript str) = rnf str `seq` ()- rnf (EvalExpr str) = rnf str `seq` ()- rnf (TargetTriple str) = rnf str `seq` ()- rnf (TargetCPU str) = rnf str `seq` ()- rnf (OptLevel i) = rnf i `seq` ()- rnf (AddOpt o) = rnf o `seq` ()- rnf (RemoveOpt o) = rnf o `seq` ()- rnf (Client str) = rnf str `seq` ()- rnf (ShowOrigErr) = ()- rnf (AutoWidth) = ()- rnf (AutoSolve) = ()- rnf (UseConsoleWidth cw) = rnf cw `seq` ()- rnf DumpHighlights = ()- rnf NoElimDeprecationWarnings = ()- rnf NoOldTacticDeprecationWarnings = ()---instance NFData TIData where- rnf TIPartial = ()- rnf (TISolution xs) = rnf xs `seq` ()--instance NFData IOption where- rnf (IOption- opt_logLevel- opt_logcats- opt_typecase- opt_typeintype- opt_coverage- opt_showimp- opt_errContext- opt_repl- opt_verbose- opt_nobanner- opt_quiet- opt_codegen- opt_outputTy- opt_ibcsubdir- opt_importdirs- opt_triple- opt_cpu- opt_cmdline- opt_origerr- opt_autoSolve- opt_autoImport- opt_optimise- opt_printdepth- opt_evaltypes- opt_desugarnats- opt_autoimpls) =- rnf opt_logLevel- `seq` rnf opt_typecase- `seq` rnf opt_typeintype- `seq` rnf opt_coverage- `seq` rnf opt_showimp- `seq` rnf opt_errContext- `seq` rnf opt_repl- `seq` rnf opt_verbose- `seq` rnf opt_nobanner- `seq` rnf opt_quiet- `seq` rnf opt_codegen- `seq` rnf opt_outputTy- `seq` rnf opt_ibcsubdir- `seq` rnf opt_importdirs- `seq` rnf opt_triple- `seq` rnf opt_cpu- `seq` rnf opt_cmdline- `seq` rnf opt_origerr- `seq` rnf opt_autoSolve- `seq` rnf opt_autoImport- `seq` rnf opt_optimise- `seq` rnf opt_printdepth- `seq` rnf opt_evaltypes- `seq` rnf opt_desugarnats- `seq` rnf opt_autoimpls- `seq` ()--instance NFData LanguageExt where- rnf TypeProviders = ()- rnf ErrorReflection = ()--instance NFData Optimisation where- rnf PETransform = ()--instance NFData ColourTheme where- rnf (ColourTheme keywordColour- boundVarColour- implicitColour- functionColour- typeColour- dataColour- promptColour- postulateColour) =- rnf keywordColour- `seq` rnf boundVarColour- `seq` rnf implicitColour- `seq` rnf functionColour- `seq` rnf typeColour- `seq` rnf dataColour- `seq` rnf promptColour- `seq` rnf postulateColour- `seq` ()--instance NFData IdrisColour where- rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()--instance NFData OutputType where- rnf Raw = ()- rnf Object = ()- rnf Executable = ()--instance NFData IBCWrite where- rnf (IBCFix fixDecl) = rnf fixDecl `seq` ()- rnf (IBCImp name) = rnf name `seq` ()- rnf (IBCStatic name) = rnf name `seq` ()- rnf (IBCClass name) = rnf name `seq` ()- rnf (IBCInstance b1 b2 n1 n2) = rnf b1 `seq` rnf b2 `seq` rnf n1 `seq` rnf n2 `seq` ()- rnf (IBCDSL name) = rnf name `seq` ()- rnf (IBCData name) = rnf name `seq` ()- rnf (IBCOpt name) = rnf name `seq` ()- rnf (IBCMetavar name) = rnf name `seq` ()- rnf (IBCSyntax syntax) = rnf syntax `seq` ()- rnf (IBCKeyword string) = rnf string `seq` ()- rnf (IBCImport imp) = rnf imp `seq` ()- rnf (IBCImportDir filePath) = rnf filePath `seq` ()- rnf (IBCObj codegen filePath) = rnf codegen `seq` rnf filePath `seq` ()- rnf (IBCLib codegen string) = rnf codegen `seq` rnf string `seq` ()- rnf (IBCCGFlag codegen string) = rnf codegen `seq` rnf string `seq` ()- rnf (IBCDyLib string) = rnf string `seq` ()- rnf (IBCHeader codegen string) = rnf codegen `seq` rnf string `seq` ()- rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` ()- rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` ()- rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()- rnf (IBCInjective name inj) = rnf name `seq` rnf inj `seq` ()- rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()- rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()- rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()- rnf (IBCErrRev terms) = rnf terms `seq` ()- rnf (IBCCG name) = rnf name `seq` ()- rnf (IBCDoc name) = rnf name `seq` ()- rnf (IBCCoercion name) = rnf name `seq` ()- rnf (IBCDef name) = rnf name `seq` ()- rnf (IBCNameHint names) = rnf names `seq` ()- rnf (IBCLineApp filePath int pTerm) = rnf filePath `seq` rnf int `seq` rnf pTerm `seq` ()- rnf (IBCErrorHandler name) = rnf name `seq` ()- rnf (IBCFunctionErrorHandler n1 n2 n3) = rnf n1 `seq` rnf n2 `seq` rnf n3 `seq` ()- rnf (IBCPostulate name) = rnf name `seq` ()- rnf (IBCExtern extern) = rnf extern `seq` ()- rnf (IBCTotCheckErr fc string) = rnf fc `seq` rnf string `seq` ()- rnf (IBCParsedRegion fc) = rnf fc `seq` ()- rnf (IBCModDocs name) = rnf name `seq` ()- rnf (IBCUsage usage) = rnf usage `seq` ()- rnf (IBCExport name) = rnf name `seq` ()- rnf (IBCAutoHint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()- rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()- rnf (IBCRecord x) = rnf x `seq` ()- rnf (IBCFragile n1 n2) = rnf n1 `seq` rnf n2 `seq` ()- rnf (IBCConstraint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()---instance NFData a => NFData (D.Block a) where- rnf (D.Para lines) = rnf lines `seq` ()- rnf (D.Header i lines) = rnf i `seq` rnf lines `seq` ()- rnf (D.Blockquote bs) = rnf bs `seq` ()- rnf (D.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()- rnf (D.CodeBlock attr txt tm) = rnf attr `seq` rnf txt `seq` ()- rnf (D.HtmlBlock txt) = rnf txt `seq` ()- rnf D.HRule = ()--instance NFData a => NFData (D.Inline a) where- rnf (D.Str txt) = rnf txt `seq` ()- rnf D.Space = ()- rnf D.SoftBreak = ()- rnf D.LineBreak = ()- rnf (D.Emph xs) = rnf xs `seq` ()- rnf (D.Strong xs) = rnf xs `seq` ()- rnf (D.Code xs tm) = rnf xs `seq` rnf tm `seq` ()- rnf (D.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()- rnf (D.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()- rnf (D.Entity a) = rnf a `seq` ()- rnf (D.RawHtml x) = rnf x `seq` ()- instance NFData CT.ListType where rnf (CT.Bullet c) = rnf c `seq` () rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()@@ -354,373 +41,65 @@ rnf CT.PeriodFollowing = () rnf CT.ParenFollowing = () -instance NFData DocTerm where- rnf Unchecked = ()- rnf (Checked x1) = rnf x1 `seq` ()- rnf (Example x1) = rnf x1 `seq` ()- rnf (Failing x1) = rnf x1 `seq` ()---- All generated by 'derive'--instance NFData SizeChange where- rnf Smaller = ()- rnf Same = ()- rnf Bigger = ()- rnf Unknown = ()--instance NFData FnInfo where- rnf (FnInfo x1) = rnf x1 `seq` ()--instance NFData Codegen where- rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf Bytecode = ()--instance NFData IRFormat where- rnf _ = ()--instance NFData LogCat where- rnf _ = ()--instance NFData CGInfo where- rnf (CGInfo x1 x2 x3)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` ()--instance NFData Fixity where- rnf (Infixl x1) = rnf x1 `seq` ()- rnf (Infixr x1) = rnf x1 `seq` ()- rnf (InfixN x1) = rnf x1 `seq` ()- rnf (PrefixN x1) = rnf x1 `seq` ()--instance NFData FixDecl where- rnf (Fix x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData Static where- rnf Static = ()- rnf Dynamic = ()--instance NFData ArgOpt where- rnf _ = ()--instance NFData Plicity where- rnf (Imp x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf (Exp x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (Constraint x1 x2)- = rnf x1 `seq` rnf x2 `seq` ()- rnf (TacImp x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()--instance NFData FnOpt where- rnf Inlinable = ()- rnf TotalFn = ()- rnf PartialFn = ()- rnf CoveringFn = ()- rnf Coinductive = ()- rnf AssertTotal = ()- rnf Dictionary = ()- rnf Implicit = ()- rnf NoImplicit = ()- rnf (CExport x1) = rnf x1 `seq` ()- rnf ErrorHandler = ()- rnf ErrorReverse = ()- rnf Reflection = ()- rnf (Specialise x1) = rnf x1 `seq` ()- rnf Constructor = ()- rnf AutoHint = ()- rnf PEGenerated = ()--instance NFData DataOpt where- rnf Codata = ()- rnf DefaultEliminator = ()- rnf DefaultCaseFun = ()- rnf DataErrRev = ()--instance (NFData t) => NFData (PDecl' t) where- rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PTy x1 x2 x3 x4 x5 x6 x7 x8)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()- rnf (PPostulate x1 x2 x3 x4 x5 x6 x7 x8)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()- rnf (PClauses x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PData x1 x2 x3 x4 x5 x6)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()- rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (POpenInterfaces x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq`- rnf x6 `seq`- rnf x7 `seq`- rnf x8 `seq`- rnf x9 `seq`- rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()- rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11 x12)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq`- rnf x6 `seq`- rnf x7 `seq`- rnf x8 `seq`- rnf x9 `seq`- rnf x10 `seq`- rnf x11 `seq` rnf x12 `seq` ()- rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq`- rnf x6 `seq`- rnf x7 `seq`- rnf x8 `seq`- rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()- rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PDirective x1) = ()- rnf (PProvider x1 x2 x3 x4 x5 x6)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq` rnf x6 `seq` ()- rnf (PTransform x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PRunElabDecl x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()--instance NFData t => NFData (ProvideWhat' t) where- rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()- rnf (ProvPostulate tm) = rnf tm `seq` ()--instance NFData PunInfo where- rnf x = x `seq` ()--instance (NFData t) => NFData (PClause' t) where- rnf (PClause x1 x2 x3 x4 x5 x6)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()- rnf (PWith x1 x2 x3 x4 x5 x6 x7)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()- rnf (PClauseR x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PWithR x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()--instance (NFData t) => NFData (PData' t) where- rnf (PDatadecl x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PLaterdecl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()--instance NFData PTerm where- rnf (PQuote x1) = rnf x1 `seq` ()- rnf (PRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()- rnf (PInferRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()- rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PLam _ x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PPi x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf (PLet _ x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PWithApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PResolveTC x1) = rnf x1 `seq` ()- rnf (PRewrite x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf (PPair x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` x5 `seq` ()- rnf (PDPair x1 x2 x3 x4 x5 x6)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` x6 `seq` ()- rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PAlternative x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PHidden x1) = rnf x1 `seq` ()- rnf (PType fc) = rnf fc `seq` ()- rnf (PUniverse _) = ()- rnf (PGoal x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PConstant x1 x2) = x1 `seq` x2 `seq` ()- rnf Placeholder = ()- rnf (PDoBlock x1) = rnf x1 `seq` ()- rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PReturn x1) = rnf x1 `seq` ()- rnf (PMetavar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PProof x1) = rnf x1 `seq` ()- rnf (PTactics x1) = rnf x1 `seq` ()- rnf (PElabError x1) = rnf x1 `seq` ()- rnf PImpossible = ()- rnf (PCoerced x1) = rnf x1 `seq` ()- rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PUnifyLog x1) = rnf x1 `seq` ()- rnf (PNoImplicits x1) = rnf x1 `seq` ()- rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (PUnquote x1) = rnf x1 `seq` ()- rnf (PQuoteName x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (PConstSugar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData PAltType where- rnf (ExactlyOne x1) = rnf x1 `seq` ()- rnf FirstSuccess = ()- rnf TryImplicit = ()--instance (NFData t) => NFData (PTactic' t) where- rnf (Intro x1) = rnf x1 `seq` ()- rnf Intros = ()- rnf (Focus x1) = rnf x1 `seq` ()- rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (Rewrite x1) = rnf x1 `seq` ()- rnf DoUnify = ()- rnf (Induction x1) = rnf x1 `seq` ()- rnf (CaseTac x1) = rnf x1 `seq` ()- rnf (Equiv x1) = rnf x1 `seq` ()- rnf (Claim x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (MatchRefine x1) = rnf x1 `seq` ()- rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (Exact x1) = rnf x1 `seq` ()- rnf Compute = ()- rnf Trivial = ()- rnf TCInstance = ()- rnf (ProofSearch r r1 r2 x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf Solve = ()- rnf Attack = ()- rnf ProofState = ()- rnf ProofTerm = ()- rnf Undo = ()- rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (ApplyTactic x1) = rnf x1 `seq` ()- rnf (ByReflection x1) = rnf x1 `seq` ()- rnf (Reflect x1) = rnf x1 `seq` ()- rnf (Fill x1) = rnf x1 `seq` ()- rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf Qed = ()- rnf Abandon = ()- rnf (TCheck x1) = rnf x1 `seq` ()- rnf (TEval x1) = rnf x1 `seq` ()- rnf (TDocStr x1) = x1 `seq` ()- rnf (TSearch x1) = rnf x1 `seq` ()- rnf Skip = ()- rnf (TFail x1) = rnf x1 `seq` ()- rnf SourceFC = ()- rnf Unfocus = ()--instance (NFData t) => NFData (PDo' t) where- rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (DoBind x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (DoLet x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()--instance (NFData t) => NFData (PArg' t) where- rnf (PImp x1 x2 x3 x4 x5)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()- rnf (PExp x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PConstraint x1 x2 x3 x4)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()- rnf (PTacImplicit x1 x2 x3 x4 x5)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()--instance NFData ClassInfo where- rnf (CI x1 x2 x3 x4 x5 x6 x7)- = rnf x1 `seq`- rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()--instance NFData RecordInfo where- rnf (RI x1 x2 x3)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()--instance NFData OptInfo where- rnf (Optimise x1 x2)- = rnf x1 `seq` rnf x2 `seq` ()--instance NFData TypeInfo where- rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()--instance (NFData t) => NFData (DSL' t) where- rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq`- rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()--instance NFData SynContext where- rnf PatternSyntax = ()- rnf TermSyntax = ()- rnf AnySyntax = ()--instance NFData Syntax where- rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()- rnf (DeclRule x1 x2) = rnf x1 `seq` rnf x2 `seq` ()--instance NFData SSymbol where- rnf (Keyword x1) = rnf x1 `seq` ()- rnf (Symbol x1) = rnf x1 `seq` ()- rnf (Binding x1) = rnf x1 `seq` ()- rnf (Expr x1) = rnf x1 `seq` ()- rnf (SimpleExpr x1) = rnf x1 `seq` ()--instance NFData Using where- rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()- rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()+instance NFData DynamicLib where+ rnf (Lib x _) = rnf x `seq` () -instance NFData SyntaxInfo where- rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)- = rnf x1 `seq`- rnf x2 `seq`- rnf x3 `seq`- rnf x4 `seq`- rnf x5 `seq`- rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()+instance NFData IdrisColour where+ rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` () +-- Handle doesn't have an NFData instance instance NFData OutputMode where- rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong+ rnf (RawOutput x) = () rnf (IdeMode x y) = rnf x `seq` () -instance NFData DefaultTotality where- rnf DefaultCheckingTotal = ()- rnf DefaultCheckingPartial = ()- rnf DefaultCheckingCovering = ()--instance NFData IState where- rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20- x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40- x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60- x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77)- = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`- rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`- rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`- rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` rnf x77 `seq` ()+instance NFData a => NFData (D.Docstring a)+instance NFData ConsoleWidth+instance NFData PrimFn+instance NFData SyntaxRules+instance NFData Opt+instance NFData TIData+instance NFData IOption+instance NFData LanguageExt+instance NFData Optimisation+instance NFData ColourTheme+instance NFData OutputType+instance NFData IBCWrite+instance NFData a => NFData (D.Block a)+instance NFData a => NFData (D.Inline a)+instance NFData DocTerm+instance NFData SizeChange+instance NFData FnInfo+instance NFData Codegen+instance NFData IRFormat+instance NFData LogCat+instance NFData CGInfo+instance NFData Fixity+instance NFData FixDecl+instance NFData Static+instance NFData ArgOpt+instance NFData Plicity+instance NFData FnOpt+instance NFData DataOpt+instance NFData Directive+instance (NFData t) => NFData (PDecl' t)+instance NFData t => NFData (ProvideWhat' t)+instance NFData PunInfo+instance (NFData t) => NFData (PClause' t)+instance (NFData t) => NFData (PData' t)+instance NFData PTerm+instance NFData PAltType+instance (NFData t) => NFData (PTactic' t)+instance (NFData t) => NFData (PDo' t)+instance (NFData t) => NFData (PArg' t)+instance NFData ClassInfo+instance NFData RecordInfo+instance NFData OptInfo+instance NFData TypeInfo+instance (NFData t) => NFData (DSL' t)+instance NFData SynContext+instance NFData Syntax+instance NFData SSymbol+instance NFData Using+instance NFData SyntaxInfo+instance NFData DefaultTotality+instance NFData IState
src/Idris/Delaborate.hs view
@@ -8,7 +8,7 @@ {-# LANGUAGE PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Delaborate (- annName, bugaddr, delab, delab', delabMV, delabSugared+ annName, bugaddr, delab, delabDirect, delab', delabMV, delabSugared , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab , pprintDelabTy, pprintErr, resugar ) where@@ -81,30 +81,50 @@ -- | Delaborate a term without resugaring delab :: IState -> Term -> PTerm-delab i tm = delab' i tm False False+delab i tm = delab' i tm False False delabMV :: IState -> Term -> PTerm-delabMV i tm = delab' i tm False True+delabMV i tm = delab' i tm False True +-- | Delaborate a term directly, leaving case applications as they are.+-- We need this for interactive case splitting, where we need access to the+-- underlying function in a delaborated form, to generate the right patterns+delabDirect :: IState -> Term -> PTerm+delabDirect i tm = delabTy' i [] tm False False False+ delabTy :: IState -> Name -> PTerm delabTy i n = case lookupTy n (tt_ctxt i) of (ty:_) -> case lookupCtxt n (idris_implicits i) of- (imps:_) -> delabTy' i imps ty False False- _ -> delabTy' i [] ty False False+ (imps:_) -> delabTy' i imps ty False False True+ _ -> delabTy' i [] ty False False True [] -> error "delabTy: got non-existing name" delab' :: IState -> Term -> Bool -> Bool -> PTerm-delab' i t f mvs = delabTy' i [] t f mvs+delab' i t f mvs = delabTy' i [] t f mvs True delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any -> Term -> Bool -- ^ use full names -> Bool -- ^ Don't treat metavariables specially+ -> Bool -- ^ resugar cases -> PTerm-delabTy' ist imps tm fullname mvs = de [] imps tm+delabTy' ist imps tm fullname mvs docases = de [] imps tm where un = fileFC "(val)"+ + -- Special case for spotting applications of case functions+ -- (Normally the scrutinee is let-bound, but hole types get normalised,+ -- so they could appear in this form. The scrutinee is always added as+ -- the last argument,+ -- although that's not always the thing that gets pattern matched+ -- in the elaborated block)+ de env imps sc+ | docases+ , isCaseApp sc+ , (P _ cOp _, args@(_:_)) <- unApply sc+ , Just caseblock <- delabCase env imps (last args) cOp args + = caseblock de env _ (App _ f a) = deFn env f [a] de env _ (V i) | i < length env = PRef un [] (snd (env!!i))@@ -141,9 +161,10 @@ = PPi expl n NoFC (de env [] ty) (de ((n,n):env) [] sc) de env imps (Bind n (Let ty val) sc)- | isCaseApp sc+ | docases+ , isCaseApp sc , (P _ cOp _, args) <- unApply sc- , Just caseblock <- delabCase env imps n val cOp args = caseblock+ , Just caseblock <- delabCase env imps val cOp args = caseblock | otherwise = PLet un n NoFC (de env [] ty) (de env [] val) (de ((n,n):env) [] sc) de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc@@ -206,8 +227,8 @@ isCN (SN (CaseN _ _)) = True isCN _ = False - delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm- delabCase env imps scvar scrutinee caseName caseArgs =+ delabCase :: [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm+ delabCase env imps scrutinee caseName caseArgs = do cases <- case lookupCtxt caseName (idris_patdefs ist) of [(cases, _)] -> return cases _ -> Nothing@@ -247,8 +268,8 @@ = case lookupTy n (tt_ctxt i) of (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $ case lookupCtxt n (idris_implicits i) of- (imps:_) -> resugar i $ delabTy' i imps ty False False- _ -> resugar i $ delabTy' i [] ty False False+ (imps:_) -> resugar i $ delabTy' i imps ty False False True+ _ -> resugar i $ delabTy' i [] ty False False True [] -> error "pprintDelabTy got a name that doesn't exist" pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
src/Idris/Docs.hs view
@@ -69,49 +69,62 @@ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation-pprintFD ist totalityFlag nsFlag (FD n doc args ty f)- = nest 4 (prettyName True nsFlag [] n <+> colon <+>- pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args- , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>- -- show doc- renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>- -- show fixity- maybe empty (\f -> text (show f) <> line) f <>- -- show arguments doc- let argshow = showArgs args [] in- (if not (null argshow)- then nest 4 $ text "Arguments:" <$> vsep argshow- else empty) <>- -- show totality status- let totality = getTotality in- (if totalityFlag && not (null totality) then- line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)- else- empty))+pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =+ nest 4 (prettyName True nsFlag [] n+ <+> colon+ <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args+ , not (T.isPrefixOf (T.pack "__") n') ] infixes ty+ -- show doc+ <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc+ -- show fixity+ <$> maybe empty (\f -> text (show f) <> line) f+ -- show arguments doc+ <> let argshow = showArgs args [] in+ (if not (null argshow)+ then nest 4 $ text "Arguments:" <$> vsep argshow+ else empty)+ -- show totality status+ <> let totality = getTotality in+ (if totalityFlag && not (null totality)+ then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)+ else empty)) - where ppo = ppOptionIst ist- infixes = idris_infixes ist- showArgs ((n, ty, Exp {}, Just d):args) bnd- = bindingOf n False <+> colon <+>- pprintPTerm ppo bnd [] infixes ty <>- showDoc ist d <> line- :- showArgs args ((n, False):bnd)- showArgs ((n, ty, Constraint {}, Just d):args) bnd- = text "Class constraint" <+>- pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line- :- showArgs args ((n, True):bnd)- showArgs ((n, ty, Imp {}, Just d):args) bnd- = text "(implicit)" <+>- bindingOf n True <+> colon <+>- pprintPTerm ppo bnd [] infixes ty <>- showDoc ist d <> line- :- showArgs args ((n, True):bnd)- showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)- showArgs [] _ = []- getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)+ where+ ppo = ppOptionIst ist++ infixes = idris_infixes ist++ -- Recurse over and show the Function's Documented arguments+ showArgs ((n, ty, Exp {}, Just d):args) bnd = -- Explicitly bound.+ bindingOf n False+ <+> colon+ <+> pprintPTerm ppo bnd [] infixes ty+ <> showDoc ist d+ <> line : showArgs args ((n, False):bnd)+ showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Class constraints.+ text "Class constraint"+ <+> pprintPTerm ppo bnd [] infixes ty+ <> showDoc ist d+ <> line : showArgs args ((n, True):bnd)+ showArgs ((n, ty, Imp {}, Just d):args) bnd = -- Implicit arguments.+ text "(implicit)"+ <+> bindingOf n True+ <+> colon+ <+> pprintPTerm ppo bnd [] infixes ty+ <> showDoc ist d+ <> line : showArgs args ((n, True):bnd)+ showArgs ((n, ty, TacImp{}, Just d):args) bnd = -- Tacit implicits+ text "(auto implicit)"+ <+> bindingOf n True+ <+> colon+ <+> pprintPTerm ppo bnd [] infixes ty+ <> showDoc ist d+ <> line : showArgs args ((n, True):bnd)+ showArgs ((n, _, _, _):args) bnd = -- Anything else+ showArgs args ((n, True):bnd)+ showArgs [] _ = [] -- end of arguments++ getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist) pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation pprintFDWithTotality ist = pprintFD ist True
src/Idris/Docstrings.hs view
@@ -6,7 +6,7 @@ Maintainer : The Idris Community. -} -{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}+{-# LANGUAGE DeriveFunctor, DeriveGeneric, ScopedTypeVariables #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Docstrings ( Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring@@ -30,7 +30,7 @@ import Data.Traversable (Traversable) import qualified Data.Sequence as S -import Control.DeepSeq (NFData(..))+import GHC.Generics (Generic) import Text.Blaze.Html (Html) @@ -39,7 +39,7 @@ | Checked Term | Example Term | Failing Err- deriving Show+ deriving (Show, Generic) -- | Render a term in the documentation renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation@@ -53,7 +53,7 @@ -- | Representation of Idris's inline documentation. The type paramter -- represents the type of terms that are associated with code blocks. data Docstring a = DocString CT.Options (Blocks a)- deriving (Show, Functor, Foldable, Traversable)+ deriving (Show, Functor, Foldable, Traversable, Generic) type Blocks a = S.Seq (Block a) @@ -65,7 +65,7 @@ | CodeBlock CT.CodeAttr T.Text a | HtmlBlock T.Text | HRule- deriving (Show, Functor, Foldable, Traversable)+ deriving (Show, Functor, Foldable, Traversable, Generic) data Inline a = Str T.Text | Space@@ -78,7 +78,7 @@ | Image (Inlines a) T.Text T.Text | Entity T.Text | RawHtml T.Text- deriving (Show, Functor, Foldable, Traversable)+ deriving (Show, Functor, Foldable, Traversable, Generic) type Inlines a = S.Seq (Inline a)
src/Idris/Elab/Clause.hs view
@@ -84,7 +84,8 @@ -- question: CAFs in where blocks? tclift $ tfail $ At fc (NoTypeDecl n) [ty] -> return ty- let atys = map snd (getArgTys fty)+ let atys_in = map snd (getArgTys (normalise ctxt [] fty))+ let atys = map (\x -> (x, isCanonical x ctxt)) atys_in cs_elab <- mapM (elabClause info opts) (zip [0..] cs) ctxt <- getContext@@ -670,7 +671,9 @@ (do pbinds ist lhs_tm -- proof search can use explicitly written names mapM_ addPSname (allNamesIn lhs_in)- mapM_ setinj (nub (tcparams ++ inj))+ ulog <- getUnifyLog+ traceWhen ulog ("Setting injective: " ++ show (nub (tcparams ++ inj))) $+ mapM_ setinj (nub (tcparams ++ inj)) setNextName (ElabResult _ _ is ctxt' newDecls highlights newGName) <- errAt "right hand side of " fname (Just clhsty)
src/Idris/Elab/Term.hs view
@@ -310,7 +310,7 @@ apt <- expandToArity t itm <- if not pattern then insertImpLam ina apt else return apt ct <- insertCoerce ina itm- t' <- insertLazy ct+ t' <- insertLazy ina ct g <- goal tm <- get_term ps <- get_probs@@ -624,7 +624,7 @@ do patvar n update_term liftPats highlightSource fc (AnnBoundName n False)- else if (defined && not guarded)+ else if defined then do apply (Var n) [] annot <- findHighlight n solve@@ -834,6 +834,7 @@ ty <- goal fty <- get_type (Var f) ctxt <- get_context+ let dataCon = isDConName f ctxt annot <- findHighlight f mapM_ checkKnownImplicit args_in let args = insertScopedImps fc (normalise ctxt env fty) args_in@@ -849,7 +850,8 @@ then -- simple app, as below do simple_app False (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))- (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))+ (elabE (ina { e_inarg = True,+ e_guarded = dataCon }) (Just fc) (getTm (head args))) (show tm) solve mapM (uncurry highlightSource) $@@ -873,7 +875,8 @@ ns <- apply (Var f) (map isph args) -- trace ("ns is " ++ show ns) $ return () -- mark any type class arguments as injective- when (not pattern) $ mapM_ checkIfInjective (map snd ns)+-- when (not pattern) $ + mapM_ checkIfInjective (map snd ns) unifyProblems -- try again with the new information, -- to help with disambiguation ulog <- getUnifyLog@@ -882,7 +885,8 @@ mapM (uncurry highlightSource) $ (ffc, annot) : map (\f -> (f, annot)) hls - elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf,+ e_guarded = dataCon }) [] fc False f (zip ns (unmatchableArgs ++ repeat False)) (f == sUN "Force")@@ -909,8 +913,7 @@ ivs' <- get_instances -- Attempt to resolve any type classes which have 'complete' types, -- i.e. no holes in them- when (not pattern || (e_inarg ina && not tcgen &&- not (e_guarded ina))) $+ when (not pattern || (e_inarg ina && not tcgen)) $ mapM_ (\n -> do focus n g <- goal env <- get_env@@ -962,7 +965,9 @@ -- maybe we can solve more things now... ulog <- getUnifyLog probs <- get_probs- traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $+ inj <- get_inj+ traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj + ++ "\nProblems: " ++ qshow probs) $ unifyProblems probs <- get_probs traceWhen ulog (qshow probs) $ return ()@@ -1409,14 +1414,14 @@ -- first. We need to do this brute force approach, rather than anything -- more precise, since there may be various other ambiguities to resolve -- first.- insertLazy :: PTerm -> ElabD PTerm- insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t- insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t- insertLazy (PCoerced t) = return t- -- Don't add a delay to pattern variables, since they can be forced- -- on the rhs- insertLazy t@(PPatvar _ _) | pattern = return t- insertLazy t =+ insertLazy :: ElabCtxt -> PTerm -> ElabD PTerm+ insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t+ insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t+ insertLazy ina (PCoerced t) = return t+ -- Don't add a delay to top level pattern variables, since they + -- can be forced on the rhs if needed+ insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t+ insertLazy ina t = do ty <- goal env <- get_env let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)@@ -1923,11 +1928,13 @@ in (ns, lhs', Impossible)) clauses' let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''+ let argtys = map (\x -> (x, isCanonical x ctxt))+ (map snd (getArgTys (normalise ctxt [] ty))) ctxt'<- lift $ addCasedef n (const []) info False (STerm Erased) True False -- TODO what are these?- (map snd $ getArgTys ty) [] -- TODO inaccessible types+ argtys [] -- TODO inaccessible types clauses' clauses''' clauses'''@@ -2007,15 +2014,27 @@ getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc getRetTy ty = ty + elabScriptStuck :: Term -> ElabD a+ elabScriptStuck x = lift . tfail $ ElabScriptStuck x+++ -- Should be dependent+ tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]+ tacTmArgs l t args | length args == l = return args+ | otherwise = elabScriptStuck t -- Probably should be an argument size mismatch internal error++ -- | Do a step in the reflected elaborator monad. The input is the -- step, the output is the (reflected) term returned. runTacTm :: Term -> ElabD Term- runTacTm (unApply -> tac@(P _ n _, args))- | n == tacN "Prim__Solve", [] <- args- = do solve+ runTacTm tac@(unApply -> (P _ n _, args))+ | n == tacN "Prim__Solve"+ = do ~[] <- tacTmArgs 0 tac args -- patterns are irrefutable because `tacTmArgs` returns lists of exactly the size given to it as first argument+ solve returnUnit- | n == tacN "Prim__Goal", [] <- args- = do hs <- get_holes+ | n == tacN "Prim__Goal"+ = do ~[] <- tacTmArgs 0 tac args+ hs <- get_holes case hs of (h : _) -> do t <- goal fmap fst . checkClosed $@@ -2024,15 +2043,18 @@ [] -> lift . tfail . Msg $ "Elaboration is complete. There are no goals." - | n == tacN "Prim__Holes", [] <- args- = do hs <- get_holes+ | n == tacN "Prim__Holes"+ = do ~[] <- tacTmArgs 0 tac args+ hs <- get_holes fmap fst . checkClosed $ mkList (Var $ reflm "TTName") (map reflectName hs)- | n == tacN "Prim__Guess", [] <- args- = do g <- get_guess+ | n == tacN "Prim__Guess"+ = do ~[] <- tacTmArgs 0 tac args+ g <- get_guess fmap fst . checkClosed $ reflect g- | n == tacN "Prim__LookupTy", [n] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__LookupTy"+ = do ~[name] <- tacTmArgs 1 tac args+ n' <- reifyTTName name ctxt <- get_context let getNameTypeAndType = \case Function ty _ -> (Ref, ty) TyDecl nt ty -> (nt, ty)@@ -2053,20 +2075,23 @@ , raw_apply (Var pairTy) [ Var (reflm "NameType") , Var (reflm "TT")]]) defs- | n == tacN "Prim__LookupDatatype", [name] <- args- = do n' <- reifyTTName name+ | n == tacN "Prim__LookupDatatype"+ = do ~[name] <- tacTmArgs 1 tac args+ n' <- reifyTTName name datatypes <- get_datatypes ctxt <- get_context fmap fst . checkClosed $ rawList (Var (tacN "Datatype")) (map reflectDatatype (buildDatatypes ist n'))- | n == tacN "Prim__LookupFunDefn", [name] <- args- = do n' <- reifyTTName name+ | n == tacN "Prim__LookupFunDefn"+ = do ~[name] <- tacTmArgs 1 tac args+ n' <- reifyTTName name fmap fst . checkClosed $ rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT")) (map reflectFunDefn (buildFunDefns ist n'))- | n == tacN "Prim__LookupArgs", [name] <- args- = do n' <- reifyTTName name+ | n == tacN "Prim__LookupArgs"+ = do ~[name] <- tacTmArgs 1 tac args+ n' <- reifyTTName name let listTy = Var (sNS (sUN "List") ["List", "Prelude"]) listFunArg = RApp listTy (Var (tacN "FunArg")) -- Idris tuples nest to the right@@ -2089,37 +2114,45 @@ (Var (tacN "FunArg")) , Var (reflm "Raw")]]) out- | n == tacN "Prim__SourceLocation", [] <- args- = fmap fst . checkClosed $- reflectFC fc- | n == tacN "Prim__Namespace", [] <- args- = fmap fst . checkClosed $- rawList (RConstant StrType) (map (RConstant . Str) ns)- | n == tacN "Prim__Env", [] <- args- = do env <- get_env+ | n == tacN "Prim__SourceLocation"+ = do ~[] <- tacTmArgs 0 tac args+ fmap fst . checkClosed $+ reflectFC fc+ | n == tacN "Prim__Namespace"+ = do ~[] <- tacTmArgs 0 tac args+ fmap fst . checkClosed $+ rawList (RConstant StrType) (map (RConstant . Str) ns)+ | n == tacN "Prim__Env"+ = do ~[] <- tacTmArgs 0 tac args+ env <- get_env fmap fst . checkClosed $ reflectEnv env- | n == tacN "Prim__Fail", [_a, errs] <- args- = do errs' <- eval errs+ | n == tacN "Prim__Fail"+ = do ~[_a, errs] <- tacTmArgs 2 tac args+ errs' <- eval errs parts <- reifyReportParts errs' lift . tfail $ ReflectionError [parts] (Msg "")- | n == tacN "Prim__PureElab", [_a, tm] <- args- = return tm- | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args- = do first' <- eval first+ | n == tacN "Prim__PureElab"+ = do ~[_a, tm] <- tacTmArgs 2 tac args+ return tm+ | n == tacN "Prim__BindElab"+ = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args+ first' <- eval first res <- eval =<< runTacTm first' next <- eval (App Complete andThen res) runTacTm next- | n == tacN "Prim__Try", [_a, first, alt] <- args- = do first' <- eval first+ | n == tacN "Prim__Try"+ = do ~[_a, first, alt] <- tacTmArgs 3 tac args+ first' <- eval first alt' <- eval alt try' (runTacTm first') (runTacTm alt') True- | n == tacN "Prim__Fill", [raw] <- args- = do raw' <- reifyRaw =<< eval raw+ | n == tacN "Prim__Fill"+ = do ~[raw] <- tacTmArgs 1 tac args+ raw' <- reifyRaw =<< eval raw apply raw' [] returnUnit | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"- , [raw, argSpec] <- args- = do raw' <- reifyRaw =<< eval raw+ = do ~[raw, argSpec] <- tacTmArgs 2 tac args+ raw' <- reifyRaw =<< eval raw argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec let op = if n == tacN "Prim__Apply" then apply@@ -2131,89 +2164,105 @@ (reflectName n1, reflectName n2) | (n1, n2) <- ns ]- | n == tacN "Prim__Gensym", [hint] <- args- = do hintStr <- eval hint+ | n == tacN "Prim__Gensym"+ = do ~[hint] <- tacTmArgs 1 tac args+ hintStr <- eval hint case hintStr of Constant (Str h) -> do n <- getNameFrom (sMN 0 h) fmap fst $ get_type_val (reflectName n) _ -> fail "no hint"- | n == tacN "Prim__Claim", [n, ty] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__Claim"+ = do ~[n, ty] <- tacTmArgs 2 tac args+ n' <- reifyTTName n ty' <- reifyRaw ty claim n' ty' returnUnit- | n == tacN "Prim__Check", [env', raw] <- args- = do env <- reifyEnv env'+ | n == tacN "Prim__Check"+ = do ~[env', raw] <- tacTmArgs 2 tac args+ env <- reifyEnv env' raw' <- reifyRaw =<< eval raw ctxt <- get_context (tm, ty) <- lift $ check ctxt env raw' fmap fst . checkClosed $ rawPair (Var (reflm "TT"), Var (reflm "TT")) (reflect tm, reflect ty)- | n == tacN "Prim__Attack", [] <- args- = do attack+ | n == tacN "Prim__Attack"+ = do ~[] <- tacTmArgs 0 tac args+ attack returnUnit- | n == tacN "Prim__Rewrite", [rule] <- args- = do r <- reifyRaw rule+ | n == tacN "Prim__Rewrite"+ = do ~[rule] <- tacTmArgs 1 tac args+ r <- reifyRaw rule rewrite r returnUnit- | n == tacN "Prim__Focus", [what] <- args- = do n' <- reifyTTName what+ | n == tacN "Prim__Focus"+ = do ~[what] <- tacTmArgs 1 tac args+ n' <- reifyTTName what hs <- get_holes if elem n' hs then focus n' >> returnUnit else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"- | n == tacN "Prim__Unfocus", [what] <- args- = do n' <- reifyTTName what+ | n == tacN "Prim__Unfocus"+ = do ~[what] <- tacTmArgs 1 tac args+ n' <- reifyTTName what movelast n' returnUnit- | n == tacN "Prim__Intro", [mn] <- args- = do n <- case fromTTMaybe mn of+ | n == tacN "Prim__Intro"+ = do ~[mn] <- tacTmArgs 1 tac args+ n <- case fromTTMaybe mn of Nothing -> return Nothing Just name -> fmap Just $ reifyTTName name intro n returnUnit- | n == tacN "Prim__Forall", [n, ty] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__Forall"+ = do ~[n, ty] <- tacTmArgs 2 tac args+ n' <- reifyTTName n ty' <- reifyRaw ty forall n' Nothing ty' returnUnit- | n == tacN "Prim__PatVar", [n] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__PatVar"+ = do ~[n] <- tacTmArgs 1 tac args+ n' <- reifyTTName n patvar' n' returnUnit- | n == tacN "Prim__PatBind", [n] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__PatBind"+ = do ~[n] <- tacTmArgs 1 tac args+ n' <- reifyTTName n patbind n' returnUnit- | n == tacN "Prim__LetBind", [n, ty, tm] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__LetBind"+ = do ~[n, ty, tm] <- tacTmArgs 3 tac args+ n' <- reifyTTName n ty' <- reifyRaw ty tm' <- reifyRaw tm letbind n' ty' tm' returnUnit- | n == tacN "Prim__Compute", [] <- args- = do compute ; returnUnit- | n == tacN "Prim__Normalise", [env, tm] <- args- = do env' <- reifyEnv env+ | n == tacN "Prim__Compute"+ = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit+ | n == tacN "Prim__Normalise"+ = do ~[env, tm] <- tacTmArgs 2 tac args+ env' <- reifyEnv env tm' <- reifyTT tm ctxt <- get_context let out = normaliseAll ctxt env' (finalise tm') fmap fst . checkClosed $ reflect out- | n == tacN "Prim__Whnf", [tm] <- args- = do tm' <- reifyTT tm+ | n == tacN "Prim__Whnf"+ = do ~[tm] <- tacTmArgs 1 tac args+ tm' <- reifyTT tm ctxt <- get_context fmap fst . checkClosed . reflect $ whnf ctxt tm'- | n == tacN "Prim__Converts", [env, tm1, tm2] <- args- = do env' <- reifyEnv env+ | n == tacN "Prim__Converts"+ = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args+ env' <- reifyEnv env tm1' <- reifyTT tm1 tm2' <- reifyTT tm2 ctxt <- get_context lift $ converts ctxt env' tm1' tm2' returnUnit- | n == tacN "Prim__DeclareType", [decl] <- args- = do (RDeclare n args res) <- reifyTyDecl decl+ | n == tacN "Prim__DeclareType"+ = do ~[decl] <- tacTmArgs 1 tac args+ (RDeclare n args res) <- reifyTyDecl decl ctxt <- get_context let rty = foldr mkPi res args (checked, ty') <- lift $ check ctxt [] rty@@ -2225,12 +2274,14 @@ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) : new_tyDecls e } returnUnit- | n == tacN "Prim__DefineFunction", [decl] <- args- = do defn <- reifyFunDefn decl+ | n == tacN "Prim__DefineFunction"+ = do ~[decl] <- tacTmArgs 1 tac args+ defn <- reifyFunDefn decl defineFunction defn returnUnit- | n == tacN "Prim__DeclareDatatype", [decl] <- args- = do RDeclare n args resTy <- reifyTyDecl decl+ | n == tacN "Prim__DeclareDatatype"+ = do ~[decl] <- tacTmArgs 1 tac args+ RDeclare n args resTy <- reifyTyDecl decl ctxt <- get_context let tcTy = foldr mkPi resTy args (checked, ty') <- lift $ check ctxt [] tcTy@@ -2240,8 +2291,9 @@ set_context ctxt' updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e } returnUnit- | n == tacN "Prim__DefineDatatype", [defn] <- args- = do RDefineDatatype n ctors <- reifyRDataDefn defn+ | n == tacN "Prim__DefineDatatype"+ = do ~[defn] <- tacTmArgs 1 tac args+ RDefineDatatype n ctors <- reifyRDataDefn defn ctxt <- get_context tyconTy <- case lookupTyExact n ctxt of Just t -> return t@@ -2264,24 +2316,28 @@ -- the rest happens in a bit updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e } returnUnit- | n == tacN "Prim__AddInstance", [cls, inst] <- args- = do className <- reifyTTName cls+ | n == tacN "Prim__AddInstance"+ = do ~[cls, inst] <- tacTmArgs 2 tac args+ className <- reifyTTName cls instName <- reifyTTName inst updateAux $ \e -> e { new_tyDecls = RAddInstance className instName : new_tyDecls e } returnUnit- | n == tacN "Prim__IsTCName", [n] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__IsTCName"+ = do ~[n] <- tacTmArgs 1 tac args+ n' <- reifyTTName n case lookupCtxtExact n' (idris_classes ist) of Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"]) Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])- | n == tacN "Prim__ResolveTC", [fn] <- args- = do g <- goal+ | n == tacN "Prim__ResolveTC"+ = do ~[fn] <- tacTmArgs 1 tac args+ g <- goal fn <- reifyTTName fn resolveTC' False True 100 g fn ist returnUnit- | n == tacN "Prim__Search", [depth, hints] <- args- = do d <- eval depth+ | n == tacN "Prim__Search"+ = do ~[depth, hints] <- tacTmArgs 2 tac args+ d <- eval depth hints' <- eval hints case (d, unList hints') of (Constant (I i), Just hs) ->@@ -2293,8 +2349,9 @@ (Constant (I _), Nothing ) -> lift . tfail . InternalMsg $ "Not a list: " ++ show hints' (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d- | n == tacN "Prim__RecursiveElab", [goal, script] <- args- = do goal' <- reifyRaw goal+ | n == tacN "Prim__RecursiveElab"+ = do ~[goal, script] <- tacTmArgs 2 tac args+ goal' <- reifyRaw goal ctxt <- get_context script <- eval script (goalTT, goalTy) <- lift $ check ctxt [] goal'@@ -2327,8 +2384,9 @@ fmap fst . checkClosed $ rawPair (Var $ reflm "TT", Var $ reflm "TT") (tm', ty')- | n == tacN "Prim__Metavar", [n] <- args- = do n' <- reifyTTName n+ | n == tacN "Prim__Metavar"+ = do ~[n] <- tacTmArgs 1 tac args+ n' <- reifyTTName n ctxt <- get_context ptm <- get_term -- See documentation above in the elab case for PMetavar@@ -2338,8 +2396,9 @@ defer unique_used mvn solve returnUnit- | n == tacN "Prim__Fixity", [op'] <- args- = do opTm <- eval op'+ | n == tacN "Prim__Fixity"+ = do ~[op'] <- tacTmArgs 1 tac args+ opTm <- eval op' case opTm of Constant (Str op) -> let opChars = ":!#$%&*+./<=>?@\\^|-~"@@ -2352,11 +2411,12 @@ [f] -> fmap fst . checkClosed $ reflectFixity f many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm- | n == tacN "Prim__Debug", [ty, msg] <- args- = do msg' <- eval msg+ | n == tacN "Prim__Debug"+ = do ~[ty, msg] <- tacTmArgs 2 tac args+ msg' <- eval msg parts <- reifyReportParts msg debugElaborator parts- runTacTm x = lift . tfail $ ElabScriptStuck x+ runTacTm x = elabScriptStuck x -- Running tactics directly -- if a tactic adds unification problems, return an error@@ -2540,7 +2600,7 @@ focus script ptm <- get_term elab ist toplevel ERHS [] (sMN 0 "tac")- (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])+ (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True True)]) (script', _) <- get_type_val (Var scriptvar) -- now that we have the script apply -- it to the reflected goal
src/Idris/IBC.hs view
@@ -49,7 +49,7 @@ import Debug.Trace ibcVersion :: Word16-ibcVersion = 144+ibcVersion = 145 -- | When IBC is being loaded - we'll load different things (and omit -- different structures/definitions) depending on which phase we're in.
src/Idris/Parser.hs view
@@ -1569,7 +1569,7 @@ parseImports fname input = do i <- getIState case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of- Failure err -> fail (show err)+ Failure (ErrInfo err _) -> fail (show err) Success (x, annots, i) -> do putIState i fname' <- runIO $ Dir.makeAbsolute fname@@ -1631,7 +1631,7 @@ parseProg syn fname input mrk = do i <- getIState case runparser mainProg i fname input of- Failure doc -> do -- FIXME: Get error location from trifecta+ Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta -- this can't be the solution! -- Issue #1575 on the issue tracker. -- https://github.com/idris-lang/Idris-dev/issues/1575
src/Idris/Parser/Expr.hs view
@@ -829,6 +829,9 @@ ; @ -}++data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm+ recordType :: SyntaxInfo -> IdrisParser PTerm recordType syn = do kw <- reservedFC "record"@@ -836,7 +839,7 @@ fgs <- fieldGetOrSet lchar '}' fc <- getFC- rec <- optional (simpleExpr syn)+ rec <- optional (do notEndApp; simpleExpr syn) highlightP kw AnnKeyword case fgs of Left fields ->@@ -854,28 +857,34 @@ Just v -> return (getAll fc (reverse fields) v) <?> "record setting expression"- where fieldSet :: IdrisParser ([Name], PTerm)+ where fieldSet :: IdrisParser ([Name], SetOrUpdate) fieldSet = do ns <- fieldGet- lchar '='- e <- expr syn- return (ns, e)+ (do lchar '='+ e <- expr syn+ return (ns, FieldSet e))+ <|> do symbol "$="+ e <- expr syn+ return (ns, FieldUpdate e) <?> "field setter" fieldGet :: IdrisParser [Name] fieldGet = sepBy1 (fst <$> fnName) (symbol "->") - fieldGetOrSet :: IdrisParser (Either [([Name], PTerm)] [Name])+ fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name]) fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',') return (Left fs)) <|> do f <- fieldGet return (Right f) - applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm+ applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm applyAll fc [] x = x applyAll fc ((ns, e) : es) x = applyAll fc es (doUpdate fc ns e x) - doUpdate fc [n] e get+ doUpdate fc ns (FieldUpdate e) get+ = let get' = getAll fc (reverse ns) get in+ doUpdate fc ns (FieldSet (PApp fc e [pexp get'])) get+ doUpdate fc [n] (FieldSet e) get = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get] doUpdate fc (n : ns) e get = PApp fc (PRef fc [] (mkType n))
src/Idris/Parser/Helpers.hs view
@@ -58,6 +58,21 @@ deriving instance Parsing IdrisInnerParser +#if MIN_VERSION_base(4,9,0)+instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where+ line = lift line+ {-# INLINE line #-}+ position = lift position+ {-# INLINE position #-}+ slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s+ {-# INLINE slicedWith #-}+ rend = lift rend+ {-# INLINE rend #-}+ restOfLine = lift restOfLine+ {-# INLINE restOfLine #-}++#endif+ #if MIN_VERSION_base(4,8,0) instance {-# OVERLAPPING #-} TokenParsing IdrisParser where #else
src/Idris/Prover.hs view
@@ -39,7 +39,7 @@ import Idris.Output import Idris.TypeSearch (searchByType) -import Text.Trifecta.Result(Result(..))+import Text.Trifecta.Result(Result(..), ErrInfo(..)) import System.IO (Handle, stdin, stdout, hPutStrLn) import System.Console.Haskeline@@ -325,7 +325,7 @@ (d, prev', st, done, prf', env', res) <- idrisCatch (case cmd of- Failure err ->+ Failure (ErrInfo err _) -> return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err) Success (Left cmd') -> case cmd' of@@ -440,7 +440,7 @@ _ -> return () (d, st, done, prf', res) <- idrisCatch (case cmd of- Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)+ Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err) Success Undo -> do (_, st) <- elabStep e loadState return (True, st, False, init prf, Right $ iPrintResult "") Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
src/Idris/REPL.hs view
@@ -80,7 +80,7 @@ import Data.List (groupBy) import qualified Data.Text as T -import Text.Trifecta.Result(Result(..))+import Text.Trifecta.Result(Result(..), ErrInfo(..)) import System.Console.Haskeline as H import System.FilePath@@ -190,7 +190,7 @@ IO (IState, FilePath) processNetCmd orig i h fn cmd = do res <- case parseCmd i "(net)" cmd of- Failure err -> return (Left (Msg " invalid command"))+ Failure (ErrInfo err _) -> return (Left (Msg " invalid command")) Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i Success (Left err) -> return (Left (Msg err)) case res of@@ -307,7 +307,7 @@ do c <- colourise i <- getIState case parseCmd i "(input)" cmd of- Failure err -> iPrintError $ show (fixColour False err)+ Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err) Success (Right (Prove mode n')) -> idrisCatch (do process fn (Prove mode n')@@ -435,9 +435,9 @@ splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm) splitPi ist (Bind n (Pi _ t _) rest) = let (hs, c, pc) = splitPi ist rest in- ((n, t, delabTy' ist [] t False False):hs,- c, delabTy' ist [] c False False)- splitPi ist tm = ([], tm, delabTy' ist [] tm False False)+ ((n, t, delabTy' ist [] t False False True):hs,+ c, delabTy' ist [] c False False True)+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False True) -- | Get the types of a list of metavariable names mvTys :: IState -> [Name] -> [(Name, Type)]@@ -722,8 +722,8 @@ let fn = fromMaybe "" (listToMaybe inputs) c <- colourise case parseCmd i "(input)" cmd of- Failure err -> do iputStrLn $ show (fixColour c err)- return (Just inputs)+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)+ return (Just inputs) Success (Right Reload) -> reload orig inputs Success (Right Watch) ->@@ -1787,8 +1787,8 @@ mapM_ (\str -> do ist <- getIState c <- colourise case parseExpr ist str of- Failure err -> do iputStrLn $ show (fixColour c err)- runIO $ exitWith (ExitFailure 1)+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)+ runIO $ exitWith (ExitFailure 1) Success e -> process "" (Eval e)) exprs runIO exitSuccess@@ -1843,8 +1843,8 @@ execScript expr = do i <- getIState c <- colourise case parseExpr i expr of- Failure err -> do iputStrLn $ show (fixColour c err)- runIO $ exitWith (ExitFailure 1)+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)+ runIO $ exitWith (ExitFailure 1) Success term -> do ctxt <- getContext (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term res <- execute tm@@ -1879,7 +1879,7 @@ runInit h processLine i cmd input clr = case parseCmd i input cmd of- Failure err -> runIO $ print (fixColour clr err)+ Failure (ErrInfo err _) -> runIO $ print (fixColour clr err) Success (Right Reload) -> iPrintError "Init scripts cannot reload the file" Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files" Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
src/Pkg/PParser.hs view
@@ -59,6 +59,20 @@ instance HasLastTokenSpan PParser where getLastTokenSpan = return Nothing +#if MIN_VERSION_base(4,9,0)+instance {-# OVERLAPPING #-} DeltaParsing PParser where+ line = lift line+ {-# INLINE line #-}+ position = lift position+ {-# INLINE position #-}+ slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s+ {-# INLINE slicedWith #-}+ rend = lift rend+ {-# INLINE rend #-}+ restOfLine = lift restOfLine+ {-# INLINE restOfLine #-}+#endif+ #if MIN_VERSION_base(4,8,0) instance {-# OVERLAPPING #-} TokenParsing PParser where #else@@ -71,7 +85,7 @@ parseDesc fp = do p <- readFile fp case runparser pPkg defaultPkg fp p of- Failure err -> fail (show $ PP.plain err)+ Failure (ErrInfo err _) -> fail (show $ PP.plain err) Success x -> return x pPkg :: PParser PkgDesc
src/Util/DynamicLinker.hs view
@@ -5,7 +5,7 @@ License : BSD3 Maintainer : The Idris Community. -}-{-# LANGUAGE ExistentialQuantification, CPP #-}+{-# LANGUAGE ExistentialQuantification, CPP, ScopedTypeVariables #-} module Util.DynamicLinker ( ForeignFun(..) , DynamicLib(..) , tryLoadLib@@ -17,8 +17,13 @@ import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr) import System.Directory #ifndef mingw32_HOST_OS+import Control.Exception (try, IOException, throwIO)+import Data.Array (Array, inRange, bounds, (!))+import Data.Functor ((<$>))+import Data.Maybe (catMaybes) import System.Posix.DynamicLinker import System.FilePath.Posix ((</>))+import Text.Regex.TDFA #else import qualified Control.Exception as Exception (catch, IOException) import System.Win32.DLL@@ -69,13 +74,69 @@ return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found #ifndef mingw32_HOST_OS+-- Load a dynamic library on POSIX systems.+-- In the simple case, we just find the appropriate filename and call dlopen().+-- In the complicated case our "foo.so" isn't actually a library. Some of the+-- .so files on modern Linux systems are linker scripts instead. dlopen()+-- doesn't know anything about those. We need to look inside the script for the+-- actual library path and load that. This is a horrible hack, the correct+-- method would be to actually parse the scripts and execute them. The approach+-- below is what GHC does. tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)-tryLoadLib dirs lib = do filename <- libFileName dirs lib- handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]- if undl handle == nullPtr- then return Nothing- else return . Just $ Lib lib handle+tryLoadLib dirs lib = do+ filename <- libFileName dirs lib+ res :: Either IOException DL <- try $+ dlopen filename [RTLD_NOW, RTLD_GLOBAL]+ mbDL <- case res of+ Right handle -> return $ Just handle+#ifdef linux_HOST_OS+ Left ex ->+ -- dlopen failed, run a regex to see if the error message looks like it+ -- could be a linker script.+ case matchAllText invalidLibRegex (show ex) of+ (x:_) -> do+ if inRange (bounds x) 1+ then do+ -- filename above may be a relative path. Get the full path out of+ -- the error message.+ let realPath = fst $ x ! 1+ fileLines <- lines <$> readFile realPath+ -- Go down the linker script line by line looking for .so+ -- filenames and try each one.+ let matches = catMaybes $ map+ (getLastMatch . matchAllText linkerScriptRegex)+ fileLines+ mapMFirst (\f -> dlopen f [RTLD_NOW, RTLD_GLOBAL]) matches+ else return Nothing+ [] -> return Nothing+#else+ Left ex -> throwIO ex+#endif+ case mbDL of+ Just handle -> if undl handle == nullPtr+ then return Nothing+ else return . Just $ Lib lib handle+ Nothing -> return Nothing +getLastMatch :: [MatchText String] -> Maybe String+getLastMatch [] = Nothing+getLastMatch (x:_) = case bounds x of+ (low, high) -> if low > high+ then Nothing+ else Just $ fst $ x ! high++mapMFirst :: (a -> IO b) -> [a] -> IO (Maybe b)+mapMFirst f [] = return Nothing+mapMFirst f (a:as) = do res <- try (f a)+ case res of+ Left (ex :: IOException) -> mapMFirst f as+ Right res -> return $ Just res++invalidLibRegex :: Regex+invalidLibRegex = makeRegex "(([^ \t()])+\\.so([^ \t:()])*):([ \t])*(invalid ELF header|file too short)"++linkerScriptRegex :: Regex+linkerScriptRegex = makeRegex "(GROUP|INPUT) *\\( *([^ )]+)" tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun) tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn
stack.yaml view
@@ -1,7 +1,7 @@-resolver: lts-5.11+resolver: lts-6.5 packages:- - '.'+ - location: . flags: idris:@@ -10,6 +10,7 @@ extra-deps: - libffi-0.1+ - trifecta-1.6 nix: enable: false
+ test/docs004/docs004.idr view
@@ -0,0 +1,11 @@+module Main++||| Some record Foo+||| @a a type+record Foo a where+ ||| Constructor for Foo+ constructor MkFoo+ ||| A field bar+ bar : Nat+ ||| A field baz+ baz : Bool
+ test/docs004/expected view
@@ -0,0 +1,18 @@+Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a+ Constructor for Foo+ Arguments:+ (implicit) a : Type -- a type+ + bar : Nat -- A field bar+ + baz : Bool -- A field baz+ + The function is Total+Main.Foo.bar : (rec : Foo a) -> Nat+ A field bar+ + The function is Total+Main.Foo.baz : (rec : Foo a) -> Bool+ A field baz+ + The function is Total
+ test/docs004/input view
@@ -0,0 +1,3 @@+:doc MkFoo+:doc bar+:doc baz
+ test/docs004/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} --quiet --nocolor docs004.idr < input+rm *.ibc
+ test/docs005/docs005.idr view
@@ -0,0 +1,19 @@+module docs005++import Data.List++%default total++||| A foobar with an auto implicit+data Foobar : Type where+ ||| New Foo+ |||+ ||| @xs Some `xs`+ ||| @ys Some `ys`+ ||| @prf The prf+ ||| @prf1 A prf+ NewFoo : (xs : List String)+ -> (ys : List Nat)+ -> {prf1 : NonEmpty xs}+ -> {auto prf : NonEmpty ys}+ -> Foobar
+ test/docs005/expected view
@@ -0,0 +1,29 @@+Data type docs005.Foobar : Type+ A foobar with an auto implicit+ +Constructors:+ NewFoo : (xs : List String) ->+ (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar+ New Foo+ Arguments:+ xs : List String -- Some xs+ + ys : List Nat -- Some ys+ + (implicit) prf1 : NonEmpty xs -- A prf+ + (auto implicit) prf : NonEmpty ys -- The prf+ +docs005.NewFoo : (xs : List String) ->+ (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar+ New Foo+ Arguments:+ xs : List String -- Some xs+ + ys : List Nat -- Some ys+ + (implicit) prf1 : NonEmpty xs -- A prf+ + (auto implicit) prf : NonEmpty ys -- The prf+ + The function is Total
+ test/docs005/input view
@@ -0,0 +1,2 @@+:doc Foobar+:doc NewFoo
+ test/docs005/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} --quiet --nocolor docs005.idr < input+rm *.ibc
test/effects001/test021.idr view
@@ -8,27 +8,41 @@ data Count : Type where -FileIO : Type -> Type -> Type-FileIO st t = Eff t [FILE_IO st, STDIO, Count ::: STATE Int] -readFile : FileIO (OpenFile Read) (List String)-readFile = readAcc [] where- readAcc : List String -> FileIO (OpenFile Read) (List String)- readAcc acc = do e <- eof- if (not e)- then do str <- readLine- Count :- put (!(Count :- get) + 1)- readAcc (str :: acc)- else return (reverse acc)--testFile : FileIO () ()-testFile = do True <- open "testFile" Read | False => putStrLn "Error!"- fcontents <- readFile- putStrLn (show fcontents)- close- putStrLn (show !(Count :- get))+TestFileIO : Type -> Type -> Type+TestFileIO st t = Eff t [FILE st, STDIO, Count ::: STATE Int] -main : IO ()-main = run testFile +readFileCount : Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]+readFileCount = readAcc []+ where+ readAcc : List String+ -> Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]+ readAcc acc = do+ e <- eof+ if (not e)+ then do+ (Result str) <- readLine+ | (FError err) => pure (FError err)+ Count :- put (!(Count :- get) + 1)+ readAcc (str :: acc)+ else do+ let res = reverse acc+ pure $ Result res +testFile : TestFileIO () ()+testFile = do+ Success <- open "testFile" Read+ | (FError err) => do+ putStrLn "Error!"+ pure ()+ (Result fcontents) <- readFileCount+ | (FError err) => do+ close+ putStrLn "Error!"+ pure ()+ putStrLn (show fcontents)+ close+ putStrLn (show !(Count :- get)) +main : IO ()+main = run testFile
+ test/interfaces006/expected view
+ test/interfaces006/interfaces006.idr view
@@ -0,0 +1,19 @@+module Categories++infixr 9 .+interface Category (c: k -> k -> Type) where+ id: c x x+ (.): c y z -> c x y -> c x z++interface Category c => Functor (c: k -> k -> Type) (f: k -> k) where+ map: c x y -> c (f x) (f y)++infixr 1 =<<+interface Functor c m => Monad (c: k -> k -> Type) (m: k -> k) where+ return: c x (m x)+ join: c (m (m x)) (m x)+ (=<<) : c x (m y) -> c (m x) (m y)++ join = (=<<) id+ (=<<) f = join . map f+
+ test/interfaces006/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces006.idr --noprelude --check+rm -rf *.ibc
+ test/records004/expected view
@@ -0,0 +1,3 @@+"Fred"+"Joe"+"Bloggs"
+ test/records004/records004.idr view
@@ -0,0 +1,13 @@+-- Test for multiple field declarations on one line with the same type++record Person where+ constructor MkPerson+ firstName, middleName, lastName : String++fred : Person+fred = MkPerson "Fred" "Joe" "Bloggs"++main : IO ()+main = do printLn (firstName fred)+ printLn (middleName fred)+ printLn (lastName fred)
+ test/records004/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ records004.idr -o records004+./records004+rm -f records004 *.ibc
+ test/records005/expected view
@@ -0,0 +1,4 @@+1/2+Difficulty: 12+0/0+Difficulty: 12
+ test/records005/records005.idr view
@@ -0,0 +1,39 @@+record Score where+ constructor MkScore+ correct : Nat+ attempted : Nat++record GameState where+ constructor MkGameState+ score : Score+ difficulty : Nat++Show GameState where+ show st = show (correct (score st)) ++ "/" + ++ show (attempted (score st)) ++ "\n"+ ++ "Difficulty: " ++ show (difficulty st)++initState : GameState+initState = MkGameState (MkScore 0 0) 12++-- Test record update syntax++correct : GameState -> GameState+correct = record { score->correct $= (+1),+ score->attempted $= (+1) }++wrong : GameState -> GameState+wrong = record { score->attempted $= (+1) }++restart : GameState -> GameState+restart = record { score->attempted = 0,+ score->correct = 0 }+++main : IO ()+main = do let st = initState+ let st' = correct st+ let st'' = wrong st'+ printLn st''+ printLn (restart st'')+
+ test/records005/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ records005.idr -o records005+./records005+rm -f records005 *.ibc
test/runtest.hs view
@@ -130,6 +130,7 @@ -- that depend on that distinction in other contexts. -- Also rewrite newlines for consistency. norm ('\r':'\n':xs) = '\n' : norm xs+ norm ('\\':'\\':xs) = '/' : norm xs norm ('\\':xs) = '/' : norm xs norm (x : xs) = x : norm xs norm [] = []