packages feed

idris 0.99.1 → 0.99.2

raw patch · 112 files changed

+5108/−678 lines, 112 filesdep ~ieee754binary-addedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ieee754

API changes (from Hackage documentation)

- Idris.Elab.Term: isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
- Idris.Elab.Term: pruneByType :: Bool -> Env -> Term -> Type -> IState -> [PTerm] -> [PTerm]
+ Idris.Delaborate: delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm
+ Idris.Elab.Utils: isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
+ Idris.Elab.Utils: pruneByType :: Bool -> Env -> Term -> Type -> IState -> [PTerm] -> [PTerm]
+ Idris.Output: iputStr :: String -> Idris ()
+ Idris.Parser.Expr: scopedImp :: SyntaxInfo -> SyntaxInfo
- Idris.Delaborate: delabTy' :: IState -> [PArg] -> Term -> Bool -> Bool -> Bool -> PTerm
+ Idris.Delaborate: delabTy' :: IState -> [PArg] -> [(Name, Type)] -> Term -> Bool -> Bool -> Bool -> PTerm

Files

CHANGELOG.md view
@@ -1,3 +1,20 @@+# New in 0.99.2++## Library Updates+++ Added `Data.Buffer` to `base`. This allows basic manipulation of mutable+  buffers of `Bits8`, including reading from and writing to files.++## Tool Updates+++ Idris now checks the list of packages specified at the command line+  against those installed. If there is a mismatch Idris will complain.++## Miscellaneous Updates+++ Documentation updates for the new `Control.ST` library++ Various stability/efficiency fixes+ # New in 0.99.1:  ## Language updates
docs/conf.py view
@@ -59,9 +59,9 @@ # built documents. # # The short X.Y version.-version = '0.99.1'+version = '0.99.2' # The full version, including alpha/beta/rc tags.-release = '0.99.1'+release = '0.99.2'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.
docs/effects/index.rst view
@@ -6,6 +6,18 @@  A tutorial on the `Effects` package in `Idris`. +.. topic:: Effects and the ``Control.ST`` module++   There is a new module in the ``contrib`` package, ``Control.ST``, which+   provides the resource tracking facilities of `Effects` but with+   better support for creating and deleting resources, and implementing+   resources in terms of other resources.++   Unless you have a particular reason to use `Effects` you are strongly+   recommended to use ``Control.ST`` instead. There is a tutorial available+   on this site for ``Control.ST`` with several examples+   (:ref:`st-tutorial-index`).+ .. note::     The documentation for Idris has been published under the Creative
docs/effects/introduction.rst view
@@ -53,7 +53,7 @@ Hello world =========== -To give an idea of how programs with effects look in , here is the+To give an idea of how programs with effects look, here is the ubiquitous “Hello world” program, written using the ``Effects`` library:
+ docs/image/login.png view

binary file changed (absent → 10155 bytes)

+ docs/image/netstate.png view

binary file changed (absent → 17544 bytes)

docs/index.rst view
@@ -21,6 +21,7 @@     tutorial/index    faq/faq+   st/index    effects/index    proofs/index    reference/index
docs/listing/idris-prompt-helloworld.txt view
@@ -1,7 +1,7 @@ $ idris hello.idr      ____    __     _     /  _/___/ /____(_)____-    / // __  / ___/ / ___/     Version 0.99.1+    / // __  / ___/ / ___/     Version 0.99.2   _/ // /_/ / /  / (__  )      http://www.idris-lang.org/  /___/\__,_/_/  /_/____/       Type :? for help
docs/listing/idris-prompt-interp.txt view
@@ -1,7 +1,7 @@ $ idris interp.idr      ____    __     _     /  _/___/ /____(_)____-    / // __  / ___/ / ___/     Version 0.99.1+    / // __  / ___/ / ___/     Version 0.99.2   _/ // /_/ / /  / (__  )      http://www.idris-lang.org/  /___/\__,_/_/  /_/____/       Type :? for help
docs/listing/idris-prompt-start.txt view
@@ -1,7 +1,7 @@ $ idris     ____    __     _    /  _/___/ /____(_)____-   / // __  / ___/ / ___/     Version 0.99.1+   / // __  / ___/ / ___/     Version 0.99.2  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/ /___/\__,_/_/  /_/____/       Type :? for help
+ docs/st/composing.rst view
@@ -0,0 +1,774 @@+.. _composing:++************************+Composing State Machines +************************++In the previous section, we defined a ``DataStore`` interface and used it+to implement the following small program which allows a user to log in to+the store then display the store's contents;++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []+  getData = do st <- connect+               OK <- login st+                  | BadPassword => do putStrLn "Failure"+                                      disconnect st+               secret <- readSecret st+               putStrLn ("Secret is: " ++ show secret)+               logout st+               disconnect st++This function only uses one state, the store itself. Usually, though,+larger programs have lots of states, and might add, delete and update+states over the course of its execution. Here, for example, a useful+extension might be to loop forever, keeping count of the number of times+there was a login failure in a state.++Furthermore, we may have *hierarchies* of state machines, in that one+state machine could be implemented by composing several others. For+example, we can have a state machine representing the state of a +graphics system, and use this to implement a *higher level* graphics API+such as turtle graphics, which uses the graphics system plus some additional+state for the turtle.++In this section, we'll see how to work with multiple states, and how to+compose state machines to make higher level state machines. We'll begin by+seeing how to add a login failure counter to ``getData``.++Working with multiple resources+===============================++To see how to work with multiple resources, we'll modify ``getData`` so+that it loops, and counts the total number of times the user fails to+log in. For example, if we write a ``main`` program which initialises the+count to zero, a session might run as follows:++.. code::++    *LoginCount> :exec main+    Enter password: Mornington Crescent+    Secret is: "Secret Data"+    Enter password: Dollis Hill +    Failure+    Number of failures: 1+    Enter password: Mornington Crescent+    Secret is: "Secret Data"+    Enter password: Codfanglers+    Failure+    Number of failures: 2+    ...++We'll start by adding a state resource to ``getData`` to keep track of the+number of failures:++.. code-block:: idrs++  getData : (ConsoleIO m, DataStore m) =>+            (failcount : Var) -> ST m () [failcount ::: State Integer]++.. topic:: Type checking ``getData``++  If you're following along in the code, you'll find that ``getData``+  no longer compiles when you update this type. That is to be expected!+  For the moment, comment out the definition of ``getData``. We'll come back+  to it shortly.++Then, we can create a ``main`` program which initialises the state to ``0``+and invokes ``getData``, as follows:++.. code-block:: idris++  main : IO ()+  main = run (do fc <- new 0+                 getData fc+                 delete fc)++We'll start our implementation of ``getData`` just by adding the new+argument for the failure count:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) =>+            (failcount : Var) -> ST m () [failcount ::: State Integer]+  getData failcount+          = do st <- connect+               OK <- login st+                  | BadPassword => do putStrLn "Failure"+                                      disconnect st+               secret <- readSecret st+               putStrLn ("Secret is: " ++ show secret)+               logout st+               disconnect st++Unfortunately, this doesn't type check, because we have the wrong resources+for calling ``connect``. The error messages shows how the resources don't+match:++.. code-block:: idris++    When checking an application of function Control.ST.>>=:+        Error in state transition:+                Operation has preconditions: []+                States here are: [failcount ::: State Integer]+                Operation has postconditions: \result => [result ::: Store LoggedOut] ++ []+                Required result states here are: st2_fn++In other words, ``connect`` requires that there are *no* resources on+entry, but we have *one*, the failure count!  +This shouldn't be a problem, though: the required resources are a *subset* of+the resources we have, after all, and the additional resources (here, the+failure count) are not relevant to ``connect``. What we need, therefore,+is a way to temporarily *hide* the additional resource.++We can achieve this with the ``call`` function:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) =>+            (failcount : Var) -> ST m () [failcount ::: State Integer]+  getData failcount+     = do st <- call connect+          ?whatNow++Here we've left a hole for the rest of ``getData`` so that you can see the+effect of ``call``. It has removed the unnecessary parts of the resource+list for calling ``connect``, then reinstated them on return. The type of+``whatNow`` therefore shows that we've added a new resource ``st``, and still+have ``failcount`` available:++.. code-block:: idris++      failcount : Var+      m : Type -> Type+      constraint : ConsoleIO m+      constraint1 : DataStore m+      st : Var+    --------------------------------------+    whatNow : STrans m () [failcount ::: State Integer, st ::: Store LoggedOut]+                          (\result => [failcount ::: State Integer])++By the end of the function, ``whatNow`` says that we need to have finished with+``st``, but still have ``failcount`` available. We can complete ``getData``+so that it works with an additional state resource by adding ``call`` whenever+we invoke one of the operations on the data store, to reduce the list of+resources:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) =>+            (failcount : Var) -> ST m () [failcount ::: State Integer]+  getData failcount+          = do st <- call connect+               OK <- call $ login st+                  | BadPassword => do putStrLn "Failure"+                                      call $ disconnect st+               secret <- call $ readSecret st+               putStrLn ("Secret is: " ++ show secret)+               call $ logout st+               call $ disconnect st++This is a little noisy, and in fact we can remove the need for it by+making ``call`` implicit. By default, you need to add the ``call`` explicitly,+but if you import ``Control.ST.ImplicitCall``, Idris will insert ``call``+where it is necessary.++.. code-block:: idris++  import Control.ST.ImplicitCall++It's now possible to write ``getData`` exactly as before:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) =>+            (failcount : Var) -> ST m () [failcount ::: State Integer]+  getData failcount+          = do st <- connect+               OK <- login st+                  | BadPassword => do putStrLn "Failure"+                                      disconnect st+               secret <- readSecret st+               putStrLn ("Secret is: " ++ show secret)+               logout st+               disconnect st++There is a trade off here: if you import ``Control.ST.ImplicitCall`` then+functions which use multiple resources are much easier to read, because the+noise of ``call`` has gone. On the other hand, Idris has to work a little+harder to type check your functions, and as a result it can take slightly+longer, and the error messages can be less helpful.++It is instructive to see the type of ``call``:++.. code-block:: idris++    call : STrans m t sub new_f -> {auto res_prf : SubRes sub old} ->+           STrans m t old (\res => updateWith (new_f res) old res_prf)++The function being called has a list of resources ``sub``, and+there is an implicit proof, ``SubRes sub old`` that the resource list in+the function being called is a subset of the overall resource list. The+ordering of resources is allowed to change, although resources which+appear in ``old`` can't appear in the ``sub`` list more than once (you will+get a type error if you try this).++The function ``updateWith`` takes the *output* resources of the +called function, and updates them in the current resource list. It makes+an effort to preserve ordering as far as possible, although this isn't+always possible if the called function does some complicated resource+manipulation.++.. topic:: Newly created resources in called functions++   If the called function creates any new resources, these will typically+   appear at the *end* of the resource list, due to the way ``updateWith``+   works. You can see this in the type of ``whatNow`` in our incomplete+   definition of ``getData`` above.++Finally, we can update ``getData`` so that it loops, and keeps+``failCount`` updated as necessary:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) =>+            (failcount : Var) -> ST m () [failcount ::: State Integer]+  getData failcount+     = do st <- call connect+          OK <- login st+             | BadPassword => do putStrLn "Failure"+                                 fc <- read failcount+                                 write failcount (fc + 1)+                                 putStrLn ("Number of failures: " ++ show (fc + 1))+                                 disconnect st+                                 getData failcount+          secret <- readSecret st+          putStrLn ("Secret is: " ++ show secret)+          logout st+          disconnect st+          getData failcount++Note that here, we're connecting and disconnecting on every iteration.+Another way to implement this would be to ``connect`` first, then call+``getData``, and implement ``getData`` as follows:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) =>+            (st, failcount : Var) -> ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]+  getData st failcount+     = do OK <- login st+             | BadPassword => do putStrLn "Failure"+                                 fc <- read failcount+                                 write failcount (fc + 1)+                                 putStrLn ("Number of failures: " ++ show (fc + 1))+                                 getData st failcount+          secret <- readSecret st+          putStrLn ("Secret is: " ++ show secret)+          logout st+          getData st failcount++It is important to add the explicit ``{m}`` in the type of ``Store {m}+LoggedOut`` for ``st``, because this gives Idris enough information to know+which implementation of ``DataStore`` to use to find the appropriate+implementation for ``Store``. Otherwise, if we only write ``Store LoggedOut``,+there's no way to know that the ``Store`` is linked with the computation+context ``m``.++We can then ``connect`` and ``disconnect`` only once, in ``main``:++.. code-block:: idris++  main : IO ()+  main = run (do fc <- new 0+                 st <- connect+                 getData st fc+                 disconnect st+                 delete fc)++By using ``call``, and importing ``Control.ST.ImplicitCall``, we can+write programs which use multiple resources, and reduce the list of+resources as necessary when calling functions which only use a subset of+the overall resources.++Composite resources: Hierarchies of state machines+==================================================++We've now seen how to use multiple resources in one function, which is+necessary for any realistic program which manipulates state. We can think+of this as "horizontal" composition: using multiple resources at once.+We'll often also need "vertical" composition: implementing one resource+in terms of one or more other resources.++We'll see an example of this in this section. First, we'll implement a+small API for graphics, in an interface ``Draw``, supporting:++* Opening a window, creating a double-buffered surface to draw on+* Drawing lines and rectangles onto a surface+* "Flipping" buffers, displaying the surface we've just drawn onto in+  the window+* Closing a window++Then, we'll use this API to implement a higher level API for turtle graphics,+in an ``interface``.+This will require not only the ``Draw`` interface, but also a representation+of the turtle state (location, direction and pen colour).++.. topic:: SDL bindings++    For the examples in this section, you'll need to install the+    (very basic!) SDL bindings for Idris, available from+    https://github.com/edwinb/SDL-idris. These bindings implement a small+    subset of the SDL API, and are for illustrative purposes only.+    Nevertheless, they are enough to implement small graphical programs+    and demonstrate the concepts of this section.++    Once you've installed this package, you can start Idris with the+    ``-p sdl`` flag, for the SDL bindings, and the ``-p contrib`` flag,+    for the ``Control.ST`` library.++The ``Draw`` interface+----------------------++We're going to use the Idris SDL bindings for this API, so you'll need+to import ``Graphics.SDL`` once you've installed the bindings.+We'll start by defining the ``Draw`` interface, which includes a data type+representing a surface on which we'll draw lines and rectangles:++.. code-block:: idris++    interface Draw (m : Type -> Type) where +        Surface : Type++We'll need to be able to create a new ``Surface`` by opening a window:++.. code-block:: idris++    initWindow : Int -> Int -> ST m Var [add Surface]++However, this isn't quite right. It's possible that opening a window+will fail, for example if our program is running in a termina without+a windowing system available. So, somehow, ``initWindow`` needs to cope+with the possibility of failure. We can do this by returning a+``Maybe Var``, rather than a ``Var``, and only adding the ``Surface``+on success:++.. code-block:: idris++    initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]++This uses a type level function ``addIfJust``, defined in ``Control.ST``+which returns an ``Action`` that only adds a resource if the operation+succeeds (that is, returns a result of the form ``Just val``.++.. topic:: ``addIfJust`` and ``addIfRight``++  ``Control.ST`` defines functions for constructing new resources if an+  operation succeeds. As well as ``addIfJust``, which adds a resource if+  an operation returns ``Just ty``, there's also ``addIfRight``:++  .. code-block:: idris+     +     addIfJust : Type -> Action (Maybe Var)+     addIfRight : Type -> Action (Either a Var)++  Each of these is implemented in terms of the following primitive action+  ``Add``, which takes a function to construct a resource list from the result+  of an operation:++  .. code-block:: idris+  +     Add : (ty -> Resources) -> Action ty+  +  Using this, you can create your own actions to add resources +  based on the result of an operation, if required. For example,+  ``addIfJust`` is implemented as follows:++  .. code-block:: idris++     addIfJust : Type -> Action (Maybe Var)+     addIfJust ty = Add (maybe [] (\var => [var ::: ty]))++If we create windows, we'll also need to be able to delete them:++.. code-block:: idris++    closeWindow : (win : Var) -> ST m () [remove win Surface]++We'll also need to respond to events such as keypresses and mouse clicks.+The ``Graphics.SDL`` library provides an ``Event`` type for this, and+we can ``poll`` for events which returns the last event which occurred,+if any:++.. code-block:: idris++    poll : ST m (Maybe Event) []++The remaining methods of ``Draw`` are ``flip``, which flips the buffers+displaying everything that we've drawn since the previous ``flip``, and+two methods for drawing: ``filledRectangle`` and ``drawLine``.++.. code-block:: idris++    flip : (win : Var) -> ST m () [win ::: Surface]+    filledRectangle : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]+    drawLine : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]++We define colours as follows, as four components (red, green, blue, alpha):++.. code-block:: idris++  data Col = MkCol Int Int Int Int++  black : Col+  black = MkCol 0 0 0 255++  red : Col+  red = MkCol 255 0 0 255++  green : Col+  green = MkCol 0 255 0 255++  -- Also blue, yellow, magenta, cyan, white, similarly...++If you import ``Graphics.SDL``, you can implement the ``Draw`` interface+using the SDL bindings as follows:++.. code-block:: idris++  interface Draw IO where+    Surface = State SDLSurface++    initWindow x y = do Just srf <- lift (startSDL x y)+                             | pure Nothing+                        var <- new srf+                        pure (Just var)++    closeWindow win = do lift endSDL+                         delete win++    flip win = do srf <- read win+                  lift (flipBuffers srf)+    poll = lift pollEvent++    filledRectangle win (x, y) (ex, ey) (MkCol r g b a)+         = do srf <- read win+              lift $ filledRect srf x y ex ey r g b a+    drawLine win (x, y) (ex, ey) (MkCol r g b a)+         = do srf <- read win+              lift $ drawLine srf x y ex ey r g b a++In this implementation, we've used ``startSDL`` to initialise a window, which,+returns ``Nothing`` if it fails. Since the type of ``initWindow`` states that+it adds a resource when it returns a value of the form ``Just val``, we+add the surface returned by ``startSDL`` on success, and nothing on+failure.  We can only successfully initialise if ``startDSL`` succeeds.++Now that we have an implementation of ``Draw``, we can try writing some+functions for drawing into a window and execute them via the SDL bindings.+For example, assuming we have a surface ``win`` to draw onto, we can write a+``render`` function as follows which draws a line onto a black background:++.. code-block:: idris++  render : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]+  render win = do filledRectangle win (0,0) (640,480) black+                  drawLine win (100,100) (200,200) red+                  flip win++The ``flip win`` at the end is necessary because the drawing primitives+are double buffered, to prevent flicker. We draw onto one buffer, off-screen,+and display the other.  When we call ``flip``, it displays the off-screen +buffer, and creates a new off-screen buffer for drawing the next frame.++To include this in a program, we'll write a main loop which renders our+image and waits for an event to indicate the user wants to close the+application:++.. code-block:: idris++  loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]+  loop win = do render win+                Just AppQuit <- poll+                     | _ => loop win+                pure ()++Finally, we can create a main program which initialises a window, if+possible, then runs the main loop:+                +.. code-block:: idris++  drawMain : (ConsoleIO m, Draw m) => ST m () []+  drawMain = do Just win <- initWindow 640 480+                   | Nothing => putStrLn "Can't open window"+                loop win+                closeWindow win++We can try this at the REPL using ``run``:++.. code::++  *Draw> :exec run drawMain++A higher level interface: ``TurtleGraphics``+--------------------------------------------++Turtle graphics involves a "turtle" moving around the screen, drawing a line as+it moves with a "pen". A turtle has attributes describing its location, the+direction it's facing, and the current pen colour. There are commands for+moving the turtle forwards, turning through an angle, and changing the+pen colour, among other things. One possible interface would be the+following:++.. code-block:: idris++  interface TurtleGraphics (m : Type -> Type) where+    Turtle : Type++    start : Int -> Int -> ST m (Maybe Var) [addIfJust Turtle]+    end : (t : Var) -> ST m () [Remove t Turtle]++    fd : (t : Var) -> Int -> ST m () [t ::: Turtle]+    rt : (t : Var) -> Int -> ST m () [t ::: Turtle]++    penup : (t : Var) -> ST m () [t ::: Turtle]+    pendown : (t : Var) -> ST m () [t ::: Turtle]+    col : (t : Var) -> Col -> ST m () [t ::: Turtle]++    render : (t : Var) -> ST m () [t ::: Turtle]++Like ``Draw``, we have a command for initialising the turtle (here called+``start``) which might fail if it can't create a surface for the turtle to+draw on. There is also a ``render`` method, which is intended to render the+picture drawn so far in a window.  One possible program with this interface+is the following, with draws a colourful square:++.. code-block:: idris++  turtle : (ConsoleIO m, TurtleGraphics m) => ST m () []+  turtle = with ST do+              Just t <- start 640 480+                   | Nothing => putStr "Can't make turtle\n"+              col t yellow+              fd t 100; rt t 90+              col t green+              fd t 100; rt t 90+              col t red+              fd t 100; rt t 90+              col t blue+              fd t 100; rt t 90+              render t+              end t++.. topic:: ``with ST do``++  The purpose of ``with ST do`` in ``turtle`` is to disambiguate ``(>>=)``,+  which could be either the version from the ``Monad`` interface, or the+  version from ``ST``. Idris can work this out itself, but it takes time to+  try all of the possibilities, so the ``with`` clause can+  speed up type checking.++To implement the interface, we could try using ``Surface`` to represent+the surface for the turtle to draw on:++.. code-block:: idris++    implementation Draw m => TurtleGraphics m where+      Turtle = Surface {m}++Knowing that a ``Turtle`` is represented as a ``Surface``, we can use the+methods provided by ``Draw`` to implement the turtle.  Unfortunately, though,+this isn't quite enough. We need to store more information: in particular, the+turtle has several attributes which we need to store somewhere.+So, not only do we need to represent the turtle as a ``Surface``, we need+to store some additional state. We can achieve this using a *composite*+resource.++Introducing composite resources+-------------------------------++A *composite* resource is built up from a list of other resources, and+is implemented using the following type, defined by ``Control.ST``:++.. code-block:: idris++  data Composite : List Type -> Type ++If we have a composite resource, we can split it into its constituent+resources, and create new variables for each of those resources, using+the *split* function. For example:++.. code-block:: idris++  splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]+  splitComp comp = do [int, str] <- split comp+                      ?whatNow+ +The call ``split comp`` extracts the ``State Int`` and ``State String`` from+the composite resource ``comp``, and stores them in the variables ``int``+and ``str`` respectively. If we check the type of ``whatNow``, we'll see+how this has affected the resource list:++.. code-block:: idris++      int : Var+      str : Var+      comp : Var+      m : Type -> Type+    --------------------------------------+    whatNow : STrans m () [int ::: State Int, str ::: State String, comp ::: State ()]+                          (\result => [comp ::: Composite [State Int, State String]])++So, we have two new resources ``int`` and ``str``, and the type of+``comp`` has been updated to the unit type, so currently holds no data.+This is to be expected: we've just extracted the data into individual+resources after all.++Now that we've extracted the individual resources, we can manipulate them+directly (say, incrementing the ``Int`` and adding a newline to the+``String``) then rebuild the composite resource using ``combine``:++.. code-block:: idris++  splitComp : (comp : Var) ->+              ST m () [comp ::: Composite [State Int, State String]]+  splitComp comp = do [int, str] <- split comp+                      update int (+ 1)+                      update str (++ "\n")+                      combine comp [int, str]+                      ?whatNow++As ever, we can check the type of ``whatNow`` to see the effect of+``combine``:++.. code-block:: idris++      comp : Var+      int : Var+      str : Var+      m : Type -> Type+    --------------------------------------+    whatNow : STrans m () [comp ::: Composite [State Int, State String]]+                     (\result => [comp ::: Composite [State Int, State String]])++The effect of ``combine``, therefore, is to take existing+resources and merge them into one composite resource. Before we run+``combine``, the target resource must exist (``comp`` here) and must be+of type ``State ()``.++It is instructive to look at the types of ``split`` and combine to see+the requirements on resource lists they work with. The type of ``split``+is the following:++.. code-block:: idris++    split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->+            STrans m (VarList vars) res (\ vs => mkRes vs ++ updateRes res prf (State ()))++The implicit ``prf`` argument says that the ``lbl`` being split must be+a composite resource. It returns a variable list, built from the composite+resource, and the ``mkRes`` function makes a list of resources of the+appropriate types. Finally, ``updateRes`` updates the composite resource to+have the type ``State ()``.++The ``combine`` function does the inverse:++.. code-block:: idris++    combine : (comp : Var) -> (vs : List Var) ->+              {auto prf : InState comp (State ()) res} ->+              {auto var_prf : VarsIn (comp :: vs) res} ->+              STrans m () res (const (combineVarsIn res var_prf))++The implicit ``prf`` argument here ensures that the target resource ``comp``+has type ``State ()``. That is, we're not overwriting any other data.+The implicit ``var_prf`` argument is similar to ``SubRes`` in ``call``, and+ensures that every variable we're using to build the composite resource+really does exist in the current resource list.++We can use composite resources to implement our higher level ``TurtleGraphics``+API in terms of ``Draw``, and any additional resources we need.++Implementing ``Turtle``+-----------------------++Now that we've seen how to build a new resource from an existing collection,+we can implement ``Turtle`` using a composite resource, containing the+``Surface`` to draw on, and individual states for the pen colour and the+pen location and direction. We also have a list of lines, which describes+what we'll draw onto the ``Surface`` when we call ``render``:++.. code-block:: idris++  Turtle = Composite [Surface {m}, -- surface to draw on+                      State Col,  -- pen colour+                      State (Int, Int, Int, Bool), -- pen location/direction/d+                      State (List Line)] -- lines to draw on render++A ``Line`` is defined as a start location, and end location, and a colour:++.. code-block:: idris++  Line : Type+  Line = ((Int, Int), (Int, Int), Col)++To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``)+if this is impossible, we begin by initialising the drawing surface then+all of the components of the state. Finally, we combine all of these+into a composite resource for the turtle:++.. code-block:: idris++    start x y = do Just srf <- initWindow x y+                        | Nothing => pure Nothing+                   col <- new white+                   pos <- new (320, 200, 0, True)+                   lines <- new []+                   turtle <- new ()+                   combine turtle [srf, col, pos, lines]+                   pure (Just turtle)++To implement ``end``, which needs to dispose of the turtle,+we deconstruct the composite resource, close the window,+then remove each individual resource. Remember that we can only ``delete``+a ``State``, so we need to ``split`` the composite resource, close the+drawing surface cleanly with ``closeWindow``, then ``delete`` the states:++.. code-block:: idris++    end t = do [srf, col, pos, lines] <- split t+               closeWindow srf; delete col; delete pos; delete lines; delete t++For the other methods, we need to ``split`` the resource to get each+component, and ``combine`` into a composite resource when we're done.+As an example, here's ``penup``:++.. code-block:: idris++    penup t = do [srf, col, pos, lines] <- split t -- Split the composite resource+                 (x, y, d, _) <- read pos          -- Deconstruct the pen position+                 write pos (x, y, d, False)        -- Set the pen down flag to False+                 combine t [srf, col, pos, lines]  -- Recombine the components++The remaining operations on the turtle follow a similar pattern. See+``samples/ST/Graphics/Turtle.idr`` in the Idris distribution for the full+details. It remains to render the image created by the turtle:++.. code-block:: idris++    render t = do [srf, col, pos, lines] <- split t -- Split the composite resource+                  filledRectangle srf (0, 0) (640, 480) black -- Draw a background+                  drawAll srf !(read lines)         -- Render the lines drawn by the turtle+                  flip srf                          -- Flip the buffers to display the image+                  combine t [srf, col, pos, lines]+                  Just ev <- poll+                    | Nothing => render t           -- Keep going until a key is pressed+                  case ev of+                       KeyUp _ => pure ()           -- Key pressed, so quit+                       _ => render t+     where drawAll : (srf : Var) -> List Line -> ST m () [srf ::: Surface {m}]+           drawAll srf [] = pure ()+           drawAll srf ((start, end, col) :: xs)+              = do drawLine srf start end col       -- Draw a line in the appropriate colour+                   drawAll srf xs
+ docs/st/examples.rst view
@@ -0,0 +1,439 @@+.. _netexample:++***********************************+Example: Network Socket Programming+***********************************++The POSIX sockets API supports communication between processes across a+network. A *socket* represents an endpoint of a network communication, and can be+in one of several states: ++* ``Ready``, the initial state+* ``Bound``, meaning that it has been bound to an address ready for incoming+  connections+* ``Listening``, meaning that it is listening for incoming connections+* ``Open``, meaning that it is ready for sending and receiving data;+* ``Closed``, meaning that it is no longer active.++The following diagram shows how the operations provided by the API modify the+state, where ``Ready`` is the initial state:++|netstate|++If a connection is ``Open``, then we can also ``send`` messages to the+other end of the connection, and ``recv`` messages from it.++The ``contrib`` package provides a module ``Network.Socket`` which+provides primitives for creating sockets and sending and receiving+messages. It includes the following functions:++.. code-block:: idris++    bind : (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) -> IO Int+    connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> IO ResultCode+    listen : (sock : Socket) -> IO Int+    accept : (sock : Socket) -> IO (Either SocketError (Socket, SocketAddress))+    send : (sock : Socket) -> (msg  : String) -> IO (Either SocketError ResultCode)+    recv : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (String, ResultCode))+    close : Socket -> IO ()++These functions cover the state transitions in the diagram above, but+none of them explain how the operations affect the state! It's perfectly+possible, for example, to try to send a message on a socket which is+not yet ready, or to try to receive a message after the socket is closed.++Using ``ST``, we can provide a better API which explains exactly how+each operation affects the state of a connection. In this section, we'll+define a sockets API, then use it to implement an "echo" server which+responds to requests from a client by echoing back a single message sent+by the client.++Defining a ``Sockets`` interface+================================++Rather than using ``IO`` for low level socket programming, we'll implement+an interface using ``ST`` which describes precisely how each operation+affects the states of sockets, and describes when sockets are created+and removed. We'll begin by creating a type to describe the abstract state+of a socket:++.. code-block:: idris++  data SocketState = Ready | Bound | Listening | Open | Closed++Then, we'll begin defining an interface, starting with a ``Sock`` type +for representing sockets, parameterised by their current state:++.. code-block:: idris++  interface Sockets (m : Type -> Type) where+    Sock : SocketState -> Type++We create sockets using the ``socket`` method. The ``SocketType`` is defined+by the sockets library, and describes whether the socket is TCP, UDP,+or some other form. We'll use ``Stream`` for this throughout, which indicates a+TCP socket.+    +.. code-block:: idris++    socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]++Remember that ``addIfRight`` adds a resource if the result of the operation+is of the form ``Right val``. By convention in this interface, we'll use+``Either`` for operations which might fail, whether or not they might carry+any additional information about the error, so that we can consistently+use ``addIfRight`` and some other type level functions.++To define a server, once we've created a socket, we need to ``bind`` it+to a port. We can do this with the ``bind`` method:++.. code-block:: idris++    bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->+           ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]++Binding a socket might fail, for example if there is already a socket+bound to the given port, so again it returns a value of type ``Either``.+The action here uses a type level function ``or``, and says that:++* If ``bind`` fails, the socket moves to the ``Sock Closed`` state+* If ``bind`` succeeds, the socket moves to the ``Sock Bound`` state, as+  shown in the diagram above++``or`` is implemented as follows:++.. code-block:: idris++    or : a -> a -> Either b c -> a+    or x y = either (const x) (const y)++So, the type of ``bind`` could equivalently be written as:++.. code-block:: idris++    bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->+           STrans m (Either () ()) [sock ::: Sock Ready]+                        (either [sock ::: Sock Closed] [sock ::: Sock Bound])++However, using ``or`` is much more concise than this, and attempts to+reflect the state transition diagram as directly as possible while still+capturing the possibility of failure.++Once we've bound a socket to a port, we can start listening for connections+from clients:++.. code-block:: idris++    listen : (sock : Var) ->+             ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]++A socket in the ``Listening`` state is ready to accept connections from+individual clients:++.. code-block:: idris++    accept : (sock : Var) ->+             ST m (Either () Var)+                  [sock ::: Sock Listening, addIfRight (Sock Open)]++If there is an incoming connection from a client, ``accept`` adds a *new*+resource to the end of the resource list (by convention, it's a good idea+to add resources to the end of the list, because this works more tidily+with ``updateWith``, as discussed in the previous section). So, we now+have *two* sockets: one continuing to listen for incoming connections,+and one ready for communication with the client.++We also need methods for sending and receiving data on a socket:++.. code-block:: idris++    send : (sock : Var) -> String ->+           ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]+    recv : (sock : Var) ->+           ST m (Either () String) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]++Once we've finished communicating with another machine via a socket, we'll+want to ``close`` the connection and remove the socket:++.. code-block:: idris++    close : (sock : Var) ->+            {auto prf : CloseOK st} -> ST m () [sock ::: Sock st :-> Sock Closed]+    remove : (sock : Var) ->+             ST m () [Remove sock (Sock Closed)]++We have a predicate ``CloseOK``, used by ``close`` in an implicit proof+argument, which describes when it is okay to close a socket: ++.. code-block:: idris++  data CloseOK : SocketState -> Type where+       CloseOpen : CloseOK Open+       CloseListening : CloseOK Listening++That is, we can close a socket which is ``Open``, talking to another machine,+which causes the communication to terminate.  We can also close a socket which+is ``Listening`` for incoming connections, which causes the server to stop+accepting requests.++In this section, we're implementing a server, but for completeness we may+also want a client to connect to a server on another machine. We can do+this with ``connect``:++.. code-block:: idris++    connect : (sock : Var) -> SocketAddress -> Port ->+              ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]++For reference, here is the complete interface:++.. code-block:: idris++  interface Sockets (m : Type -> Type) where+    Sock : SocketState -> Type+    socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]+    bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->+           ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]+    listen : (sock : Var) ->+             ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]+    accept : (sock : Var) ->+             ST m (Either () Var) [sock ::: Sock Listening, addIfRight (Sock Open)]+    connect : (sock : Var) -> SocketAddress -> Port ->+              ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]+    close : (sock : Var) -> {auto prf : CloseOK st} ->+            ST m () [sock ::: Sock st :-> Sock Closed]+    remove : (sock : Var) -> ST m () [Remove sock (Sock Closed)]+    send : (sock : Var) -> String ->+           ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]+    recv : (sock : Var) -> +           ST m (Either () String) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]++We'll see how to implement this shortly; mostly, the methods can be implemented+in ``IO`` by using the raw sockets API directly. First, though, we'll see+how to use the API to implement an "echo" server.++Implementing an "Echo" server with ``Sockets``+==============================================++At the top level, our echo server begins and ends with no resources available,+and uses the ``ConsoleIO`` and ``Sockets`` interfaces:++.. code-block:: idris++  startServer : (ConsoleIO m, Sockets m) => ST m () []++The first thing we need to do is create a socket for binding to a port+and listening for incoming connections, using ``socket``. This might fail,+so we'll need to deal with the case where it returns ``Right sock``, where+``sock`` is the new socket variable, or wher it returns ``Left err``:++.. code-block:: idris++  startServer : (ConsoleIO m, Sockets m) => ST m () []+  startServer =+    do Right sock <- socket Stream+             | Left err => pure ()+       ?whatNow++It's a good idea to implement this kind of function interactively, step by+step, using holes to see what state the overall system is in after each+step. Here, we can see that after a successful call to ``socket``, we+have a socket available in the ``Ready`` state:++.. code-block:: idris++      sock : Var+      m : Type -> Type+      constraint : ConsoleIO m+      constraint1 : Sockets m+    --------------------------------------+    whatNow : STrans m () [sock ::: Sock Ready] (\result1 => [])++Next, we need to bind the socket to a port, and start listening for+connections. Again, each of these could fail. If they do, we'll remove+the socket. Failure always results in a socket in the ``Closed`` state,+so all we can do is ``remove`` it:++.. code-block:: idris++  startServer : (ConsoleIO m, Sockets m) => ST m () []+  startServer =+    do Right sock <- socket Stream        | Left err => pure ()+       Right ok <- bind sock Nothing 9442 | Left err => remove sock+       Right ok <- listen sock            | Left err => remove sock+       ?runServer++Finally, we have a socket which is listening for incoming connections:++.. code-block:: idris++      ok : ()+      sock : Var+      ok1 : ()+      m : Type -> Type+      constraint : ConsoleIO m+      constraint1 : Sockets m+    --------------------------------------+    runServer : STrans m () [sock ::: Sock Listening]+                       (\result1 => [])++We'll implement this in a separate function. The type of ``runServer``+tells us what the type of ``echoServer`` must be (noting that we need+to give the ``m`` argument to ``Sock`` explicitly):++.. code-block:: idris++  echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->+               ST m () [remove sock (Sock {m} Listening)]++We can complete the definition of ``startServer`` as follows:++.. code-block:: idris++  startServer : (ConsoleIO m, Sockets m) => ST m () []+  startServer =+    do Right sock <- socket Stream        | Left err => pure ()+       Right ok <- bind sock Nothing 9442 | Left err => remove sock+       Right ok <- listen sock            | Left err => remove sock+       echoServer sock++In ``echoServer``, we'll keep accepting requests and responding to them+until something fails, at which point we'll close the sockets and+return. We begin by trying to accept an incoming connection:++.. code-block:: idris++  echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->+               ST m () [remove sock (Sock {m} Listening)]+  echoServer sock =+    do Right new <- accept sock | Left err => do close sock; remove sock+       ?whatNow++If ``accept`` fails, we need to close the ``Listening`` socket and+remove it before returning, because the type of ``echoServer`` requires+this.++As always, implementing ``echoServer`` incrementally means that we can check+the state we're in as we develop. If ``accept`` succeeds, we have the+existing ``sock`` which is still listening for connections, and a ``new``+socket, which is open for communication:++.. code-block:: idris++      new : Var+      sock : Var+      m : Type -> Type+      constraint : ConsoleIO m+      constraint1 : Sockets m+    --------------------------------------+    whatNow : STrans m () [sock ::: Sock Listening, new ::: Sock Open]+                          (\result1 => [])++To complete ``echoServer``, we'll receive a message on the ``new``+socket, and echo it back. When we're done, we close the ``new`` socket,+and go back to the beginning of ``echoServer`` to handle the next+connection:++.. code-block:: idris++  echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->+               ST m () [remove sock (Sock {m} Listening)]+  echoServer sock =+    do Right new <- accept sock | Left err => do close sock; remove sock+       Right msg <- recv new | Left err => do close sock; remove sock; remove ne+       Right ok <- send new ("You said " ++ msg)+             | Left err => do remove new; close sock; remove sock+       close new; remove new; echoServer sock++Implementing ``Sockets``+========================++To implement ``Sockets`` in ``IO``, we'll begin by giving a concrete type+for ``Sock``. We can use the raw sockets API (implemented in+``Network.Sockeet``) for this, and use a ``Socket`` stored in a ``State``, no+matter what abstract state the socket is in:++.. code-block:: idris++  implementation Sockets IO where+    Sock _ = State Socket++Most of the methods can be implemented by using the raw socket API+directly, returning ``Left`` or ``Right`` as appropriate. For example,+we can implement ``socket``, ``bind`` and ``listen`` as follows:++.. code-block:: idris++    socket ty = do Right sock <- lift $ Socket.socket AF_INET ty 0+                        | Left err => pure (Left ())+                   lbl <- new sock+                   pure (Right lbl)+    bind sock addr port = do ok <- lift $ bind !(read sock) addr port+                             if ok /= 0+                                then pure (Left ())+                                else pure (Right ())+    listen sock = do ok <- lift $ listen !(read sock)+                     if ok /= 0+                        then pure (Left ())+                        else pure (Right ())++There is a small difficulty with ``accept``, however, because when we+use ``new`` to create a new resource for the open connection, it appears+at the *start* of the resource list, not the end. We can see this by+writing an incomplete definition, using ``returning`` to see what the+resources need to be if we return ``Right lbl``:++.. code-block:: idris++    accept sock = do Right (conn, addr) <- lift $ accept !(read sock)+                           | Left err => pure (Left ())+                     lbl <- new conn+                     returning (Right lbl) ?fixResources++It's convenient for ``new`` to add the resource to the beginning of the+list because, in general, this makes automatic proof construction with+an ``auto``-implicit easier for Idris. On the other hand, when we use+``call`` to make a smaller set of resources, ``updateWith`` puts newly+created resources at the *end* of the list, because in general that reduces+the amount of re-ordering of resources. ++If we look at the type of+``fixResources``, we can see what we need to do to finish ``accept``:++.. code-block:: idris++      _bindApp0 : Socket+      conn : Socket+      addr : SocketAddress+      sock : Var+      lbl : Var+    --------------------------------------+    fixResources : STrans IO () [lbl ::: State Socket, sock ::: State Socket]+                          (\value => [sock ::: State Socket, lbl ::: State Socket])++The current list of resources is ordered ``lbl``, ``sock``, and we need them+to be in the order ``sock``, ``lbl``. To help with this situation,+``Control.ST`` provides a primitive ``toEnd`` which moves a resource to the+end of the list. We can therefore complete ``accept`` as follows:++.. code-block:: idris++    accept sock = do Right (conn, addr) <- lift $ accept !(read sock)+                           | Left err => pure (Left ())+                     lbl <- new conn+                     returning (Right lbl) (toEnd lbl)++For the complete implementation of ``Sockets``, take a look at+``samples/ST/Net/Network.idr`` in the Idris distribution. You can also+find the complete echo server there, ``EchoServer.idr``. There is also+a higher level network protocol, ``RandServer.idr``, using a hierarchy of+state machines to implement a high level network communication protocol+in terms of the lower level sockets API. This also uses threading, to+handle incoming requests asyncronously. You can find some more detail+on threading and the random number server in the draft paper+`State Machines All The Way Down <https://www.idris-lang.org/drafts/sms.pdf>`_+by Edwin Brady.++.. |netstate| image:: ../image/netstate.png+                      :width: 300px+
+ docs/st/index.rst view
@@ -0,0 +1,27 @@+.. _st-tutorial-index:++##########################################################+Implementing State-aware Systems in Idris: The ST Tutorial+##########################################################++A tutorial on implementing state-aware systems using +the `Control.ST` library in `Idris`.++.. note::++   The documentation for Idris has been published under the Creative+   Commons CC0 License. As such to the extent possible under law, *The+   Idris Community* has waived all copyright and related or neighbouring+   rights to Documentation for Idris.++   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/++.. toctree::+   :maxdepth: 1++   introduction+   state+   machines+   composing+   examples+
+ docs/st/introduction.rst view
@@ -0,0 +1,93 @@+********+Overview+********++Pure functional languages with dependent types such as `Idris+<http://www.idris-lang.org/>`_ support reasoning about programs directly+in the type system, promising that we can *know* a program will run+correctly (i.e. according to the specification in its type) simply+because it compiles. ++Realistically, though,  software relies on state, and many components rely on state machines. For+example, they describe network transport protocols like TCP, and+implement event-driven systems and regular expression matching. Furthermore,+many fundamental resources like network sockets and files are, implicitly,+managed by state machines, in that certain operations are only valid on+resources in certain states, and those operations can change the states of the+underlying resource. For example, it only makes sense to send a message on a+connected network socket, and closing a socket changes its state from "open" to+"closed". State machines can also encode important security properties. For+example, in the software which implements an ATM, it’s important that the ATM+dispenses cash only when the machine is in a state where a card has been+inserted and the PIN verified.++In this tutorial we will introduce the ``Control.ST`` library, which is included+with the Idris distribution (currently as part of the ``contrib`` package)+and supports programming and reasoning with state and side effects.  This+tutorial assumes familiarity with pure programming in Idris, as described in+:ref:`tutorial-index`.+For further background information, the ``ST`` library is based on ideas+discussed in Chapter 13 (available as a free sample chapter) and Chapter 14+of `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_.++The ``ST`` library allows us to write programs which are composed of multiple+state transition systems. It supports composition in two ways: firstly, we can+use several independently implemented state transition systems at once;+secondly, we can implement one state transition system in terms of others.+++Introductory example: a data store requiring a login+====================================================++Many software components rely on some form of state, and there may be+operations which are only valid in specific states. For example, consider+a secure data store in which a user must log in before getting access to+some secret data. This system can be in one of two states:++* ``LoggedIn``, in which the user is allowed to read the secret+* ``LoggedOut``, in which the user has no access to the secret++We can provide commands to log in, log out, and read the data, as illustrated+in the following diagram:++|login|++The ``login`` command, if it succeeds, moves the overall system state from+``LoggedOut`` to ``LoggedIn``. The ``logout`` command moves the state from+``LoggedIn`` to ``LoggedOut``. Most importantly, the ``readSecret`` command+is only valid when the system is in the ``LoggedIn`` state.++We routinely use type checkers to ensure that variables and arguments are used+consistently. However, statically checking that operations are performed only+on resources in an appropriate state is not well supported by mainstream type+systems. In the data store example, for example, it's important to check that+the user is successfully logged in before using ``readSecret``. The+``ST`` library allows us to represent this kind of *protocol* in the type+system, and ensure at *compile-time* that the secret is only read when the+user is logged in.++Outline+=======++This tutorial starts (:ref:`introst`) by describing how to manipulate+individual states, introduce a data type ``STrans`` for describing stateful+functions, and ``ST`` which describes top level state transitions.+Next (:ref:`smstypes`) it describes how to represent state machines in+types, and how to define *interfaces* for describing stateful systems.+Then (:ref:`composing`) it describes how to compose systems of multiple+state machines. It explains how to implement systems which use several+state machines at once, and how to implement a high level stateful system+in terms of lower level systems.+Finally (:ref:`netexample`) we'll see a specific example of a stateful+API in practice, implementing the POSIX network sockets API.++The ``Control.ST`` library is also described in a draft paper by+`Edwin Brady <https://edwinb.wordpress.com/>`_, "State Machines All The Way+Down", available `here <https://www.idris-lang.org/drafts/sms.pdf>`_.+This paper presents many of the examples from this tutorial, and describes+the motivation, design and implementation of the library in more depth. ++.. |login| image:: ../image/login.png+                   :width: 500px++
+ docs/st/machines.rst view
@@ -0,0 +1,536 @@+.. _smstypes:++***********************+State Machines in Types+***********************++In the introduction, we saw the following state transition diagram representing+the (abstract) states of a data store, and the actions we can perform on the+store:++|login|++We say that these are the *abstract* states of the store, because the concrete+state will contain a lot more information: for example, it might contain+user names, hashed passwords, the store contents, and so on. However, as far+as we are concerned for the actions ``login``, ``logout`` and ``readSecret``, +it's whether we are logged in or not which affects which are valid.++We've seen how to manipulate states using ``ST``, and some small examples+of dependent types in states. In this section, we'll see how to use+``ST`` to provide a safe API for the data store. In the API, we'll encode+the above diagram in the types, in such a way that we can only execute the+operations ``login``, ``logout`` and ``readSecret`` when the state is+valid.++So far, we've used ``State`` and the primitive operations, ``new``, ``read``,+``write`` and ``delete`` to manipulate states. For the data store API,+however, we'll begin by defining an *interface* (see :ref:`sect-interfaces` in+the Idris tutorial) which describes the operations on the store, and explains+in their types exactly when each operation is valid, and how it affects+the store's state. By using an interface, we can be sure that +this is the *only* way to access the store.++Defining an interface for the data store+========================================++We'll begin by defining a data type, in a file ``Login.idr``, which represents+the two abstract states of the store, either ``LoggedOut`` or ``LoggedIn``:++.. code-block:: idris++    data Access = LoggedOut | LoggedIn++We can define a data type for representing the current state of a store,+holding all of the necessary information (this might be user names, hashed+passwords, store contents and so on) and parameterise it by the logged in+status of the store:++.. code-block:: idris++  Store : Access -> Type++Rather than defining a concrete type now, however, we'll include this in+a data store *interface* and define a concrete type later:++.. code-block:: idris++  interface DataStore (m : Type -> Type) where+    Store : Access -> Type++We can continue to populate this interface with operations on the store.  Among+other advantages, by separating the *interface* from its *implementation* we+can provide different concrete implementations for different contexts.+Furthermore, we can write programs which work with a store without needing+to know any details of how the store is implemented.++We'll need to be able to ``connect`` to a store, and ``disconnect`` when+we're done. Add the following methods to the ``DataStore`` interface:++.. code-block:: idris++    connect : ST m Var [add (Store LoggedOut)]+    disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]++The type of ``connect`` says that it returns a new resource which has the+initial type ``Store LoggedOut``. Conversely, ``disconnect``, given a+resource in the state ``Store LoggedOut``, removes that resource.+We can see more clearly what ``connect`` does by trying the following+(incomplete) definition:++.. code-block:: idris++  doConnect : DataStore m => ST m () []+  doConnect = do st <- connect+                 ?whatNow++Note that we're working in a *generic* context ``m``, constrained so that+there must be an implementation of ``DataStore`` for ``m`` to be able to+execute ``doConnect``.+If we check the type of ``?whatNow``, we'll see that the remaining+operations begin with a resource ``st`` in the state ``Store LoggedOut``,+and we need to finish with no resources.++.. code-block:: idris++      m : Type -> Type+      constraint : DataStore m+      st : Var+    --------------------------------------+    whatNow : STrans m () [st ::: Store LoggedOut] (\result => [])++Then, we can remove the resource using ``disconnect``:++.. code-block:: idris++  doConnect : DataStore m => ST m () []+  doConnect = do st <- connect+                 disconnect st+                 ?whatNow++Now checking the type of ``?whatNow`` shows that we have no resources+available:++.. code-block:: idris++      m : Type -> Type+      constraint : DataStore m+      st : Var+    --------------------------------------+    whatNow : STrans m () [] (\result => [])++To continue our implementation of the ``DataStore`` interface, next we'll add a+method for reading the secret data. This requires that the ``store`` is in the+state ``Store LoggedIn``:++.. code-block:: idris++    readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]++At this point we can try writing a function which connects to a store,+reads the secret, then disconnects. However, it will be unsuccessful, because+``readSecret`` requires us to be logged in:++.. code-block:: idris++  badGet : DataStore m => ST m () []+  badGet = do st <- connect+              secret <- readSecret st+              disconnect st++This results in the following error, because ``connect`` creates a new+store in the ``LoggedOut`` state, and ``readSecret`` requires the store+to be in the ``LoggedIn`` state:++.. code-block:: idris++    When checking an application of function Control.ST.>>=:+        Error in state transition:+                Operation has preconditions: [st ::: Store LoggedOut]+                States here are: [st ::: Store LoggedIn]+                Operation has postconditions: \result => []+                Required result states here are: \result => []++The error message explains how the required input states (the preconditions)+and the required output states (the postconditions) differ from the states+in the operation. In order to use ``readSecret``, we'll need a way to get+from a ``Store LoggedOut`` to a ``Store LoggedIn``. As a first attempt,+we can try the following type for ``login``:++.. code-block:: idris++    login : (store : Var) -> ST m () [store ::: Store LoggedOut :-> Store LoggedIn] -- Incorrect type!++Note that in the *interface* we say nothing about *how* ``login`` works;+merely how it affects the overall state. Even so, there is a problem with+the type of ``login``, because it makes the assumption that it will always+succeed. If it fails - for example because the implementation prompts for+a password and the user enters the password incorrectly - then it must not+result in a ``LoggedIn`` store.++Instead, therefore, ``login`` will return whether logging in was successful,+via the following type;++.. code-block:: idris++    data LoginResult = OK | BadPassword++Then, we can *calculate* the result state (see :ref:`depstate`) from the+result. Add the following method to the ``DataStore`` interface:++.. code-block:: idris++    login : (store : Var) ->+            ST m LoginResult [store ::: Store LoggedOut :->+                               (\res => Store (case res of+                                                    OK => LoggedIn+                                                    BadPassword => LoggedOut))]++If ``login`` was successful, then the state after ``login`` is+``Store LoggedIn``. Otherwise, the state is ``Store LoggedOut``.++To complete the interface, we'll add a method for logging out of the store.+We'll assume that logging out is always successful, and moves the store+from the ``Store LoggedIn`` state to the ``Store LoggedOut`` state.++.. code-block:: idris++    logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]++This completes the interface, repeated in full for reference below:++.. code-block:: idris++  interface DataStore (m : Type -> Type) where+    Store : Access -> Type++    connect : ST m Var [add (Store LoggedOut)]+    disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]++    readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]+    login : (store : Var) ->+            ST m LoginResult [store ::: Store LoggedOut :->+                               (\res => Store (case res of+                                                    OK => LoggedIn+                                                    BadPassword => LoggedOut))]+    logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]++Before we try creating any implementations of this interface, let's see how+we can write a function with it, to log into a data store, read the secret+if login is successful, then log out again.++Writing a function with the data store+======================================++As an example of working with the ``DataStore`` interface, we'll write a+function ``getData``, which connects to a store in order to read some data from+it. We'll write this function interactively, step by step, using the types of+the operations to guide its development. It has the following type:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []++This type means that there are no resources available on entry or exit.+That is, the overall list of actions is ``[]``, meaning that at least+externally, the function has no overall effect on the resources. In other+words, for every resource we create during ``getData``, we'll also need to+delete it before exit.++Since we want to use methods of the ``DataStore`` interface, we'll+constraint the computation context ``m`` so that there must be an+implementation of ``DataStore``. We also have a constraint ``ConsoleIO m``+so that we can display any data we read from the store, or any error+messages.++We start by connecting to the store, creating a new resource ``st``, then+trying to ``login``:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []+  getData = do st <- connect+               ok <- login st+               ?whatNow++Logging in will either succeed or fail, as reflected by the value of+``ok``. If we check the type of ``?whatNow``, we'll see what state the+store currently has:++.. code-block:: idris++      m : Type -> Type+      constraint : ConsoleIO m+      constraint1 : DataStore m+      st : Var+      ok : LoginResult+    --------------------------------------+    whatNow : STrans m () [st ::: Store (case ok of   +                                              OK => LoggedIn +                                              BadPassword => LoggedOut)]+                          (\result => [])++The current state of ``st`` therefore depends on the value of ``ok``,+meaning that we can make progress by case splitting on ``ok``:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []+  getData = do st <- connect+               ok <- login st+               case ok of+                    OK => ?whatNow_1+                    BadPassword => ?whatNow_2++The types of the holes in each branch, ``?whatNow_1`` and ``?whatNow_2``,+show how the state changes depending on whether logging in was successful.+If it succeeded, the store is ``LoggedIn``:++.. code-block:: idris++    --------------------------------------+    whatNow_1 : STrans m () [st ::: Store LoggedIn] (\result => [])++On the other hand, if it failed, the store is ``LoggedOut``:++.. code-block:: idris++    --------------------------------------+    whatNow_2 : STrans m () [st ::: Store LoggedOut] (\result => [])++In ``?whatNow_1``, since we've successfully logged in, we can now read+the secret and display it to the console:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []+  getData = do st <- connect+               ok <- login st+               case ok of+                    OK => do secret <- readSecret st+                             putStrLn ("Secret is: " ++ show secret)+                             ?whatNow_1+                    BadPassword => ?whatNow_2++We need to finish the ``OK`` branch with no resources available. We can+do this by logging out of the store then disconnecting:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []+  getData = do st <- connect+               ok <- login st+               case ok of+                    OK => do secret <- readSecret st+                             putStrLn ("Secret is: " ++ show secret)+                             logout st+                             disconnect st+                    BadPassword => ?whatNow_2++Note that we *must* ``logout`` of ``st`` before calling ``disconnect``,+because ``disconnect`` requires that the store is in the ``LoggedOut``+state.++Furthermore, we can't simply use ``delete`` to remove the resource, as+we did with the ``State`` examples in the previous section, because+``delete`` only works when the resource has type ``State ty``, for some+type ``ty``. If we try to use ``delete`` instead of ``disconnect``, we'll+see an error message like the following:++.. code-block:: idris++    When checking argument prf to function Control.ST.delete:+            Can't find a value of type+                    InState st (State st) [st ::: Store LoggedOut]++In other words, the type checker can't find a proof that the resource+``st`` has a type of the form ``State st``, because its type is+``Store LoggedOut``. Since ``Store`` is part of the ``DataStore`` interface,+we *can't* yet know the concrete representation of the ``Store``, so we+need to remove the resource via the interface, with ``disconnect``, rather+than directly with ``delete``.++We can complete ``getData`` as follows, using a pattern matching bind+alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a+``case`` statement to catch the possibilty of an error with ``login``:++.. code-block:: idris++  getData : (ConsoleIO m, DataStore m) => ST m () []+  getData = do st <- connect+               OK <- login st+                  | BadPassword => do putStrLn "Failure"+                                      disconnect st+               secret <- readSecret st+               putStrLn ("Secret is: " ++ show secret)+               logout st+               disconnect st++We can't yet try this out, however, because we don't have any implementations+of ``getData``! If we try to execute it in an ``IO`` context, for example,+we'll get an error saying that there's no implementation of ``DataStore IO``:++.. code::++    *Login> :exec run {m = IO} getData+    When checking an application of function Control.ST.run:+            Can't find implementation for DataStore IO++The final step in implementing a data store which correctly follows the+state transition diagram, therefore, is to provide an implementation+of ``DataStore``.++Implementing the interface+==========================++To execute ``getData`` in ``IO``, we'll need to provided an implementation+of ``DataStore`` which works in the ``IO`` context. We can begin as+follows:++.. code-block:: idris++  implementation DataStore IO where++Then, we can ask Idris to populate the interface with skeleton definitions+for the necessary methods (press ``Ctrl-Alt-A`` in Atom for "add definition"+or the corresponding shortcut for this in the Idris mode in your favourite+editor):++.. code-block:: idris++  implementation DataStore IO where+    Store x = ?DataStore_rhs_1+    connect = ?DataStore_rhs_2+    disconnect store = ?DataStore_rhs_3+    readSecret store = ?DataStore_rhs_4+    login store = ?DataStore_rhs_5+    logout store = ?DataStore_rhs_6++The first decision we'll need to make is how to represent the data store.+We'll keep this simple, and store the data as a single ``String``, using+a hard coded password to gain access. So, we can define ``Store`` as+follows, using a ``String`` to represent the data no matter whether we+are ``LoggedOut`` or ``LoggedIn``:++.. code-block:: idris++    Store x = State String++Now that we've given a concrete type for ``Store``, we can implement operations+for connecting, disconnecting, and accessing the data. And, since we used+``State``, we can use ``new``, ``delete``, ``read`` and ``write`` to+manipulate the store.++Looking at the types of the holes tells us how we need to manipulate the+state. For example, the ``?DataStore_rhs_2`` hole tells us what we need+to do to implement ``connect``. We need to return a new ``Var`` which +represents a resource of type ``State String``:++.. code-block:: idris++    --------------------------------------+    DataStore_rhs_2 : STrans IO Var [] (\result => [result ::: State String])++We can implement this by creating a new variable with some data for the+content of the store (we can use any ``String`` for this) and returning+that variable:++.. code-block:: idris++    connect = do store <- new "Secret Data"+                 pure store++For ``disconnect``, we only need to delete the resource:++.. code-block:: idris++    disconnect store = delete store++For ``readSecret``, we need to read the secret data and return the+``String``. Since we now know the concrete representation of the data is+a ``State String``, we can use ``read`` to access the data directly:++.. code-block:: idris++    readSecret store = read store++We'll do ``logout`` next and return to ``login``. Checking the hole+reveals the following:++.. code-block:: idris++      store : Var+    --------------------------------------+    DataStore_rhs_6 : STrans IO () [store ::: State String] (\result => [store ::: State String])++So, in this minimal implementation, we don't actually have to do anything!++.. code-block:: idris++    logout store = pure ()++For ``login``, we need to return whether logging in was successful. We'll+do this by prompting for a password, and returning ``OK`` if it matches+a hard coded password, or ``BadPassword`` otherwise:++.. code-block:: idris++    login store = do putStr "Enter password: "+                     p <- getStr+                     if p == "Mornington Crescent"+                        then pure OK+                        else pure BadPassword++For reference, here is the complete implementation which allows us to+execute a ``DataStore`` program at the REPL:++.. code-block:: idris++  implementation DataStore IO where+    Store x = State String+    connect = do store <- new "Secret Data"+                 pure store+    disconnect store = delete store+    readSecret store = read store+    login store = do putStr "Enter password: "+                     p <- getStr+                     if p == "Mornington Crescent"+                        then pure OK+                        else pure BadPassword+    logout store = pure ()++Finally, we can try this at the REPL as follows (Idris defaults to the+``IO`` context at the REPL if there is an implementation available, so no+need to give the ``m`` argument explicitly here):++.. code:: ++    *Login> :exec run getData+    Enter password: Mornington Crescent+    Secret is: "Secret Data"++    *Login> :exec run getData+    Enter password: Dollis Hill+    Failure++We can only use ``read``, ``write``, ``new`` and ``delete`` on a resource+with a ``State`` type. So, *within* the implementation of ``DataStore``,+or anywhere where we know the context is ``IO``, we can access the data store+however we like: this is where the internal details of ``DataStore`` are+implemented. However, if we merely have a constraint ``DataStore m``, we can't+know how the store is implemented, so we can only access via the API given+by the ``DataStore`` interface.++It is therefore good practice to use a *generic* context ``m`` for functions+like ``getData``, and constrain by only the interfaces we need, rather than+using a concrete context ``IO``.++We've now seen how to manipulate states, and how to encapsulate state+transitions for a specific system like the data store inn an interface.+However, realistic systems will need to *compose* state machines. We'll+either need to use more than one state machine at a time, or implement one+state machine in terms of one or more others. We'll see how to achieve this+in the next section.++.. |login| image:: ../image/login.png+                   :width: 500px
+ docs/st/state.rst view
@@ -0,0 +1,656 @@+.. _introst:++**********************************+Introducing ST: Working with State+**********************************++The ``Control.ST`` library provides facilities for creating, reading, writing+and destroying state in Idris functions, and tracking changes of state in+a function's type. It is based around the concept of *resources*, which are,+essentially, mutable variables, and a dependent type, ``STrans`` which tracks+how those resources change when a function runs:++.. code-block:: idris++    STrans : (m : Type -> Type) ->+             (resultType : Type) ->+             (in_res : Resources) ->+             (out_res : resultType -> Resources) ->+             Type++A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence+of actions which can manipulate state. The arguments are: ++* ``m``, which is an underlying *computation context* in which the actions will be executed.+  Usually, this will be a generic type with a ``Monad`` implementation, but +  it isn't necessarily so. In particular, there is no need to understand monads+  to be able to use ``ST`` effectively!+* ``resultType``, which is the type of the value the sequence will produce+* ``in_res``, which is a list of *resources* available *before* executing the actions.+* ``out_res``, which is a list of resources available *after* executing the actions,+  and may differ depending on the result of the actions.++We can use ``STrans`` to describe *state transition systems* in a function's+type. We'll come to the definition of ``Resources`` shortly, but for the moment+you can consider it an abstract representation of the "state of the world".+By giving the input resources (``in_res``) and the output resources+(``out_res``) we are describing the *preconditions* under which a function+is allowed to execute, and *postconditions* which describe how a function+affects the overall state of the world.++We'll begin in this section by looking at some small examples of ``STrans``+functions, and see how to execute them. We'll also introduce ``ST``,+a type-level function which allows us to describe the state transitions of+a stateful function concisely.++.. topic:: Type checking the examples++    For the examples in this section, and throughout this tutorial,+    you'll need to ``import Control.ST`` and add the ``contrib`` package by+    passing the ``-p contrib`` flag to ``idris``.+++Introductory examples: manipulating ``State``+=============================================++An ``STrans`` function explains, in its type, how it affects a collection of+``Resources``. A resource has a *label* (of type ``Var``), which we use to+refer to the resource throughout the function, and we write the state of a+resource, in the ``Resources`` list, in the form ``label ::: type``.++For example, the following function+has a resource ``x`` available on input, of type ``State Integer``, and that+resource is still a ``State Integer`` on output:++.. code-block:: idris++  increment : (x : Var) -> STrans m () [x ::: State Integer]+                                       (const [x ::: State Integer])+  increment x = do num <- read x+                   write x (num + 1)++.. sidebar:: Verbosity of the type of ``increment``++    The type of ``increment`` may seem somewhat verbose, in that the+    *input* and *output* resources are repeated, even though they are the+    same. We'll introduce a much more concise way of writing this type at the+    end of this section (:ref:`sttype`), when we describe the ``ST`` type+    itself.+                   +This function reads the value stored at the resource ``x`` with ``read``,+increments it then writes the result back into the resource ``x`` with+``write``. We'll see the types of ``read`` and ``write`` shortly +(see :ref:`stransprimops`). We can also create and delete resources:++.. code-block:: idris++  makeAndIncrement : Integer -> STrans m Integer [] (const [])+  makeAndIncrement init = do var <- new init+                             increment var+                             x <- read var+                             delete var+                             pure x++The type of ``makeAndIncrement`` states that it has *no* resources available on+entry (``[]``) or exit (``const []``). It creates a new ``State`` resource with+``new`` (which takes an initial value for the resource), increments the value,+reads it back, then deletes it using ``delete``, returning the final value+of the resource. Again, we'll see the types of ``new`` and ``delete``+shortly.++The ``m`` argument to ``STrans`` (of type ``Type -> Type``) is the *computation context* in+which the function can be run. Here, the type level variable indicates that we+can run it in *any* context. We can run it in the identity context with+``runPure``. For example, try entering the above definitions in a file+``Intro.idr`` then running the following at the REPL:++.. code:: ++    *Intro> runPure (makeAndIncrement 93)+    94 : Integer++It's a good idea to take an interactive, type-driven approach to implementing+``STrans`` programs. For example, after creating the resource with ``new init``,+you can leave a *hole* for the rest of the program to see how creating the+resource has affected the type:++.. code-block:: idris++  makeAndIncrement : Integer -> STrans m Integer [] (const [])+  makeAndIncrement init = do var <- new init+                             ?whatNext++If you check the type of ``?whatNext``, you'll see that there is now+a resource available, ``var``, and that by the end of the function there+should be no resource available:++.. code-block:: idris++      init : Integer+      m : Type -> Type+      var : Var+    --------------------------------------+    whatNext : STrans m Integer [var ::: State Integer] (\value => [])++These small examples work in any computation context ``m``. However, usually,+we are working in a more restricted context. For example, we might want to+write programs which only work in a context that supports interactive+programs. For this, we'll need to see how to *lift* operations from the+underlying context.++Lifting: Using the computation context+======================================++Let's say that, instead of passing an initial integer to ``makeAndIncrement``,+we want to read it in from the console. Then, instead of working in a generic+context ``m``, we can work in the specific context ``IO``:++.. code-block:: idris++    ioMakeAndIncrement : STrans IO () [] (const [])++This gives us access to ``IO`` operations, via the ``lift`` function. We+can define ``ioMakeAndIncrement`` as follows:++.. code-block:: idris++  ioMakeAndIncrement : STrans IO () [] (const [])+  ioMakeAndIncrement+     = do lift $ putStr "Enter a number: "+          init <- lift $ getLine+          var <- new (cast init)+          lift $ putStrLn ("var = " ++ show !(read var))+          increment var+          lift $ putStrLn ("var = " ++ show !(read var))+          delete var++The ``lift`` function allows us to use funtions from the underlying+computation context (``IO`` here) directly. Again, we'll see the exact type+of ``lift`` shortly.++.. topic:: !-notation++    In ``ioMakeAndIncrement`` we've used ``!(read var)`` to read from the+    resource. You can read about this ``!``-notation in the main Idris tutorial+    (see :ref:`monadsdo`). In short, it allows us to use an ``STrans``+    function inline, rather than having to bind the result to a variable+    first.++    Conceptually, at least, you can think of it as having the following type:++    .. code-block:: idris+    +        (!) : STrans m a state_in state_out -> a++    It is syntactic sugar for binding a variable immediately before the+    current action in a ``do`` block, then using that variable in place of+    the ``!``-expression.+++In general, though, it's bad practice to use a *specific* context like+``IO``. Firstly, it requires us to sprinkle ``lift`` liberally throughout+our code, which hinders readability. Secondly, and more importantly, it will+limit the safety of our functions, as we'll see in the next section+(:ref:`smstypes`).++So, instead, we define *interfaces* to restrict the computation context.+For example, ``Control.ST`` defines a ``ConsoleIO`` interface which+provides the necessary methods for performing basic console interaction:++.. code-block:: idris++    interface ConsoleIO (m : Type -> Type) where+      putStr : String -> STrans m () res (const res)+      getStr : STrans m String res (const res)++That is, we can write to and read from the console with any available+resources ``res``, and neither will affect the available resources.+This has the following implementation for ``IO``:++.. code-block:: idris++    ConsoleIO IO where+      putStr str = lift (Interactive.putStr str)+      getStr = lift Interactive.getLine++Now, we can define ``ioMakeAndIncrement`` as follows:++.. code-block:: idris++  ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])+  ioMakeAndIncrement+     = do putStr "Enter a number: "+          init <- getStr+          var <- new (cast init)+          putStrLn ("var = " ++ show !(read var))+          increment var+          putStrLn ("var = " ++ show !(read var))+          delete var++Instead of working in ``IO`` specifically, this works in a generic context+``io``, provided that there is an implementation of ``ConsoleIO`` for that+context. This has several advantages over the first version:++* All of the calls to ``lift`` are in the implementation of the interface,+  rather than ``ioMakeAndIncrement``+* We can provide alternative implementations of ``ConsoleIO``, perhaps+  supporting exceptions or logging in addition to basic I/O.+* As we'll see in the next section (:ref:`smstypes`), it will allow us to+  define safe APIs for manipulating specific resources more precisely.++Earlier, we used ``runPure`` to run ``makeAndIncrement`` in the identity+context. Here, we use ``run``, which allows us to execute an ``STrans`` program+in any context (as long as it has an implementation of ``Applicative``) and we+can execute ``ioMakeAndIncrement`` at the REPL as follows:++.. code:: ++    *Intro> :exec run ioMakeAndIncrement+    Enter a number: 93+    var = 93+    var = 94++.. _depstate:++Manipulating ``State`` with dependent types+===========================================++In our first example of ``State``, when we incremented the value its+*type* remained the same. However, when we're working with+*dependent* types, updating a state may also involve updating its type.+For example, if we're adding an element to a vector stored in a state,+its length will change:++.. code-block:: idris++  addElement : (vec : Var) -> (item : a) ->+               STrans m () [vec ::: State (Vect n a)]+                    (const [vec ::: State (Vect (S n) a)])+  addElement vec item = do xs <- read vec+                           write vec (item :: xs)++Note that you'll need to ``import Data.Vect`` to try this example. ++.. topic:: Updating a state directly with ``update``++    Rather than using ``read`` and ``write`` separately, you can also+    use ``update`` which reads from a ``State``, applies a function to it,+    then writes the result. Using ``update`` you could write ``addElement``+    as follows:++    .. code-block:: idris++      addElement : (vec : Var) -> (item : a) ->+                   STrans m () [vec ::: State (Vect n a)]+                        (const [vec ::: State (Vect (S n) a)])+      addElement vec item = update vec (item ::)++We don't always know *how* exactly the type will change in the course of a+sequence actions, however. For example, if we have a state containing a+vector of integers, we might read an input from the console and only add it+to the vector if the input is a valid integer. Somehow, we need a different+type for the output state depending on whether reading the integer was+successful, so neither of the following types is quite right:++.. code-block:: idris++  readAndAdd_OK : ConsoleIO io => (vec : Var) ->+                  STrans m ()  -- Returns an empty tuple+                              [vec ::: State (Vect n Integer)]+                       (const [vec ::: State (Vect (S n) Integer)])+  readAndAdd_Fail : ConsoleIO io => (vec : Var) ->+                    STrans m ()  -- Returns an empty tuple+                                [vec ::: State (Vect n Integer)]+                         (const [vec ::: State (Vect n Integer)])++Remember, though, that the *output* resource types can be *computed* from+the result of a function. So far, we've used ``const`` to note that the+output resources are always the same, but here, instead, we can use a type+level function to *calculate* the output resources. We start by returning+a ``Bool`` instead of an empty tuple, which is ``True`` if reading the input+was successful, and leave a *hole* for the output resources:++.. code-block:: idris++  readAndAdd : ConsoleIO io => (vec : Var) ->+               STrans m Bool [vec ::: State (Vect n Integer)]+                             ?output_res++If you check the type of ``?output_res``, you'll see that Idris expects+a function of type ``Bool -> Resources``, meaning that the output resource+type can be different depending on the result of ``readAndAdd``:++.. code-block:: idris++      n : Nat+      m : Type -> Type+      io : Type -> Type+      constraint : ConsoleIO io+      vec : Var+    --------------------------------------+    output_res : Bool -> Resources++So, the output resource is either a ``Vect n Integer`` if the input is+invalid (i.e. ``readAndAdd`` returns ``False``) or a ``Vect (S n) Integer``+if the input is valid. We can express this in the type as follows:++.. code-block:: idris++  readAndAdd : ConsoleIO io => (vec : Var) ->+               STrans io Bool [vec ::: State (Vect n Integer)]+                     (\res => [vec ::: State (if res then Vect (S n) Integer+                                                     else Vect n Integer)])++Then, when we implement ``readAndAdd`` we need to return the appropriate+value for the output state. If we've added an item to the vector, we need to+return ``True``, otherwise we need to return ``False``:+                                                     +.. code-block:: idris++  readAndAdd : ConsoleIO io => (vec : Var) ->+               STrans io Bool [vec ::: State (Vect n Integer)]+                     (\res => [vec ::: State (if res then Vect (S n) Integer+                                                     else Vect n Integer)])+  readAndAdd vec = do putStr "Enter a number: "+                      num <- getStr+                      if all isDigit (unpack num)+                         then do+                           update vec ((cast num) ::)+                           pure True     -- added an item, so return True+                         else pure False -- didn't add, so return False++There is a slight difficulty if we're developing interactively, which is+that if we leave a hole, the required output state isn't easily visible+until we know the value that's being returned. For example. in the following+incomplete definition of ``readAndAdd`` we've left a hole for the+successful case:++.. code-block:: idris++  readAndAdd vec = do putStr "Enter a number: "+                      num <- getStr+                      if all isDigit (unpack num)+                         then ?whatNow+                         else pure False++We can look at the type of ``?whatNow``, but it is unfortunately rather less+than informative:++.. code-block:: idris++      vec : Var+      n : Nat+      io : Type -> Type+      constraint : ConsoleIO io+      num : String+    --------------------------------------+    whatNow : STrans io Bool [vec ::: State (Vect (S n) Integer)]+                     (\res =>+                        [vec :::+                         State (ifThenElse res+                                           (Delay (Vect (S n) Integer))+                                           (Delay (Vect n Integer)))])++The problem is that we'll only know the required output state when we know+the value we're returning. To help with interactive development, ``Control.ST``+provides a function ``returning`` which allows us to specify the return+value up front, and to update the state accordingly. For example, we can+write an incomplete ``readAndAdd`` as follows:++.. code-block:: idris++  readAndAdd vec = do putStr "Enter a number: "+                      num <- getStr+                      if all isDigit (unpack num)+                         then returning True ?whatNow+                         else pure False++This states that, in the successful branch, we'll be returning ``True``, and+``?whatNow`` should explain how to update the states appropriately so that+they are correct for a return value of ``True``. We can see this by checking+the type of ``?whatNow``, which is now a little more informative:++.. code-block:: idris++      vec : Var+      n : Nat+      io : Type -> Type+      constraint : ConsoleIO io+      num : String+    --------------------------------------+    whatnow : STrans io () [vec ::: State (Vect n Integer)]+                     (\value => [vec ::: State (Vect (S n) Integer)])++This type now shows, in the output resource list of ``STrans``,+that we can complete the definition by adding an item to ``vec``, which+we can do as follows:++.. code-block:: idris++  readAndAdd vec = do putStr "Enter a number: "+                      num <- getStr+                      if all isDigit (unpack num)+                         then returning True (update vec ((cast num) ::))+                         else returning False (pure ()) -- returning False, so no state update required++.. _stransprimops:++``STrans`` Primitive operations +===============================++Now that we've written a few small examples of ``STrans`` functions, it's+a good time to look more closely at the types of the state manipulation+functions we've used. First, to read and write states, we've used+``read`` and ``write``:++.. code-block:: idris++    read : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->+           STrans m ty res (const res)+    write : (lbl : Var) -> {auto prf : InState lbl ty res} ->+            (val : ty') ->+            STrans m () res (const (updateRes res prf (State ty')))++These types may look a little daunting at first, particularly due to the+implicit ``prf`` argument, which has the following type:++.. code-block:: idris++    prf : InState lbl (State ty) res}++This relies on a predicate ``InState``. A value of type ``InState x ty res``+means that the reference ``x`` must have type ``ty`` in the list of+resources ``res``. So, in practice, all this type means is that we can+only read or write a resource if a reference to it exists in the list of+resources.++Given a resource label ``res``, and a proof that ``res`` exists in a list+of resources, ``updateRes`` will update the type of that resource. So,+the type of ``write`` states that the type of the resource will be updated+to the type of the given value.++The type of ``update`` is similar to that for ``read`` and ``write``, requiring+that the resource has the input type of the given function, and updating it to+have the output type of the function:++.. code-block:: idris++    update : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->+             (ty -> ty') ->+             STrans m () res (const (updateRes res prf (State ty')))++The type of ``new`` states that it returns a ``Var``, and given an initial+value of type ``state``, the output resources contains a new resource+of type ``State state``:++.. code-block:: idris++    new : (val : state) -> +          STrans m Var res (\lbl => (lbl ::: State state) :: res)++It's important that the new resource has type ``State state``, rather than+merely ``state``, because this will allow us to hide implementation details+of APIs. We'll see more about what this means in the next section,+:ref:`smstypes`.++The type of ``delete`` states that the given label will be removed from+the list of resources, given an implicit proof that the label exists in+the input resources:++.. code-block:: idris++    delete : (lbl : Var) -> {auto prf : InState lbl (State st) res} ->+             STrans m () res (const (drop res prf))++Here, ``drop`` is a type level function which updates the resource list,+removing the given resource ``lbl`` from the list.++We've used ``lift`` to run functions in the underlying context. It has the+following type:++.. code-block:: idris++    lift : Monad m => m t -> STrans m t res (const res)++Given a ``result`` value, ``pure`` is an ``STrans`` program which produces+that value, provided that the current list of resources is correct when+producing that value:++.. code-block:: idris++    pure : (result : ty) -> STrans m ty (out_fn result) out_fn++We can use ``returning`` to break down returning a value from an+``STrans`` functions into two parts: providing the value itself, and updating+the resource list so that it is appropriate for returning that value:++.. code-block:: idris++    returning : (result : ty) -> +                STrans m () res (const (out_fn result)) ->+                STrans m ty res out_fn++Finally, we've used ``run`` and ``runPure`` to execute ``STrans`` functions+in a specific context. ``run`` will execute a function in any context,+provided that there is an ``Applicative`` implementation for that context,+and ``runPure`` will execute a function in the identity context:++.. code-block:: idris++    run : Applicative m => STrans m a [] (const []) -> m a+    runPure : STrans Basics.id a [] (const []) -> a++Note that in each case, the input and output resource list must be empty.+There's no way to provide an initial resource list, or extract the final+resources. This is deliberate: it ensures that *all* resource management is+carried out in the controlled ``STrans`` environment and, as we'll see, this+allows us to implement safe APIs with precise types explaining exactly how+resources are tracked throughout a program.++These functions provide the core of the ``ST`` library; there are some+others which we'll encounter later, for more advanced situations, but the+functions we have seen so far already allow quite sophisticated state-aware+programming and reasoning in Idris.++.. _sttype:++`ST`: Representing state transitions directly+============================================++We've seen a few examples of small ``STrans`` functions now, and+their types can become quite verbose given that we need to provide explicit+input and output resource lists. This is convenient for giving types for+the primitive operations, but for more general use it's much more convenient+to be able to express *transitions* on individual resources, rather than+giving input and output resource lists in full. We can do this with+``ST``:++.. code-block:: idris++    ST : (m : Type -> Type) ->+         (resultType : Type) -> +         List (Action resultType) -> Type++``ST`` is a type level function which computes an appropriate ``STrans``+type given a list of *actions*, which describe transitions on resources.+An ``Action`` in a function type can take one of the following forms (plus+some others which we'll see later in the tutorial):++* ``lbl ::: ty`` expresses that the resource ``lbl`` begins and ends in+  the state ``ty``+* ``lbl ::: ty_in :-> ty_out`` expresses that the resource ``lbl`` begins+  in state ``ty_in`` and ends in state ``ty_out``+* ``lbl ::: ty_in :-> (\res -> ty_out)`` expresses that the resource ``lbl``+  begins in state ``ty_in`` and ends in a state ``ty_out``, where ``ty_out``+  is computed from the result of the function ``res``.++So, we can write some of the function types we've seen so far as follows:++.. code-block:: idris++  increment : (x : Var) -> ST m () [x ::: State Integer]++That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.++.. code-block:: idris+  +  makeAndIncrement : Int -> ST m Int []++That is, ``makeAndIncrement`` begins and ends with no resources.++.. code-block:: idris++  addElement : (vec : Var) -> (item : a) ->+               ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]++That is, ``addElement`` changes ``vec`` from ``State (Vect n a)`` to+``State (Vect (S n) a)``.++.. code-block:: idris++  readAndAdd : ConsoleIO io => (vec : Var) ->+               ST io Bool+                     [vec ::: State (Vect n Integer) :->+                      \res => State (if res then Vect (S n) Integer+                                            else Vect n Integer)]++By writing the types in this way, we express the minimum necessary to explain+how each function affects the overall resource state. If there is a resource+update depending on a result, as with ``readAndAdd``, then we need to describe+it in full. Otherwise, as with ``increment`` and ``makeAndIncrement``, we can+write the input and output resource lists without repetition.++An ``Action`` can also describe *adding* and *removing* states:++* ``add ty``, assuming the operation returns a ``Var``, adds a new resource+  of type ``ty``.+* ``remove lbl ty`` expresses that the operation removes the resource named+  ``lbl``, beginning in state ``ty`` from the resource list.++So, for example, we can write:++.. code-block:: idris++  newState : ST m Var [add (State Int)]+  removeState : (lbl : Var) -> ST m () [remove lbl (State Int)]++The first of these, ``newState``, returns a new resource label, and adds that+resource to the list with type ``State Int``. The second, ``removeState``,+given a label ``lbl``, removes the resource from the list. These types are+equivalent to the following:++.. code-block:: idris++  newState : STrans m Var [] (\lbl => [lbl ::: State Int])+  removeState : (lbl : Var) -> STrans m () [lbl ::: State Int] (const [])++These are the primitive methods of constructing an ``Action``.  Later, we will+encounter some other ways using type level functions to help with readability.++In the remainder of this tutorial, we will generally use ``ST`` except on+the rare occasions we need the full precision of ``STrans``. In the next+section, we'll see how to use the facilities provided by ``ST`` to write+a precise API for a system with security properties: a data store requiring+a login.++
docs/tutorial/interfaces.rst view
@@ -203,6 +203,8 @@         pure  : a -> f a         (<*>) : f (a -> b) -> f a -> f b +.. _monadsdo:+ Monads and ``do``-notation ==========================
docs/tutorial/modules.rst view
@@ -301,9 +301,8 @@     "[1, 2, 3, 4, 5, 6]" : String  -********************** Modules Dependencies Using Atom -**********************+===============================  If you are using the Atom editor and have a dependency on another package,  corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,
idris.cabal view
@@ -1,5 +1,5 @@ Name:           idris-Version:        0.99.1+Version:        0.99.2 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -270,7 +270,7 @@                 , filepath < 1.5                 , fingertree >= 0.1 && < 0.2                 , haskeline >= 0.7 && < 0.8-                , ieee754 >= 0.7 && < 0.8+                , ieee754 >= 0.7 && <= 0.8.0                 , mtl >= 2.1 && < 2.3                 , network < 2.7                 , optparse-applicative >= 0.11 && < 0.14
libs/base/Control/Catchable.idr view
@@ -4,7 +4,7 @@  %access public export -interface Catchable (m : Type -> Type) t where+interface Catchable (m : Type -> Type) t | m where     throw : t -> m a     catch : m a -> (t -> m a) -> m a
+ libs/base/Data/Buffer.idr view
@@ -0,0 +1,119 @@+module Data.Buffer++%include C "idris_buffer.h"++||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory+export+record Buffer where+  constructor MkBuffer+  ||| Raw bytes, as a pointer to a block of memory+  rawdata : ManagedPtr -- let Idris run time manage the memory+  ||| Cached size of block+  buf_size : Int+  ||| Next location to read/write (e.g. when reading from file)+  location : Int ++||| Create a new buffer 'size' bytes long. Returns 'Nothing' if allocation+||| fails+export+newBuffer : (size : Int) -> IO (Maybe Buffer)+newBuffer size = do bptr <- foreign FFI_C "idris_newBuffer" (Int -> IO Ptr) +                                    size+                    bad <- nullPtr bptr+                    if bad then pure Nothing+                           else pure (Just (MkBuffer (prim__registerPtr bptr (size + 8)) size 0))++||| Reset the 'next location' pointer of the buffer to 0.+||| The 'next location' pointer gives the location for the next file read/write+||| so resetting this means you can write it again+export+resetBuffer : Buffer -> Buffer+resetBuffer buf = record { location = 0 } buf++||| Return the space available in the buffer+export+rawSize : Buffer -> IO Int+rawSize b = foreign FFI_C "idris_getBufferSize" (ManagedPtr -> IO Int) (rawdata b)++export+size : Buffer -> Int+size b = buf_size b++||| Set the byte at position 'loc' to 'val'.+||| Does nothing if the location is outside the bounds of the buffer+export+setByte : Buffer -> (loc : Int) -> (val : Bits8) -> IO ()+setByte b loc val+    = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())+              (rawdata b) loc val++||| Set the byte at position 'loc' to 'val'.+||| Does nothing if the location is out of bounds of the buffer, or the string+||| is too long for the location+export+setString : Buffer -> Int -> String -> IO ()+setString b loc val+    = foreign FFI_C "idris_setBufferString" (ManagedPtr -> Int -> String -> IO ())+              (rawdata b) loc val++||| Copy data from 'src' to 'dest'. Reads 'len' bytes starting at position+||| 'start' in 'src', and writes them starting at position 'loc' in 'dest'.+||| Does nothing if a location is out of bounds, or there is not enough room+export+copyData : (src : Buffer) -> (start, len : Int) ->+           (dest : Buffer) -> (loc : Int) -> IO ()+copyData src start len dest loc +    = foreign FFI_C "idris_copyBuffer" (ManagedPtr -> Int -> Int -> ManagedPtr -> Int -> IO ())+              (rawdata src) start len (rawdata dest) loc++||| Return the value at the given location in the buffer+export+getByte : Buffer -> (loc : Int) -> IO Bits8+getByte b loc+    = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)+              (rawdata b) loc ++||| Read 'maxbytes' into the buffer from a file, returning a new+||| buffer with the 'locaton' pointer moved along+export+readBufferFromFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer+readBufferFromFile (FHandle h) buf max+    = do numread <- foreign FFI_C "idris_readBuffer" (Ptr -> ManagedPtr -> Int -> Int -> IO Int)+                       h (rawdata buf) (location buf) max+         pure (record { location $= (+numread) } buf)++||| Write 'maxbytes' from the buffer from a file, returning a new+||| buffer with the 'locaton' pointer moved along+export+writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer+writeBufferToFile (FHandle h) buf max+    = do let maxwrite = size buf - location buf+         let max' = if maxwrite < max then maxwrite else max+         foreign FFI_C "idris_writeBuffer" (Ptr -> ManagedPtr -> Int -> Int -> IO ())+                 h (rawdata buf) (location buf) max'+         pure (record { location $= (+max') } buf)++||| Return the contents of the buffer as a list+export+bufferData : Buffer -> IO (List Bits8)+bufferData b = do let len = size b+                  unpackTo [] len+  where unpackTo : List Bits8 -> Int -> IO (List Bits8)+        unpackTo acc 0 = pure acc+        unpackTo acc loc = do val <- getByte b (loc - 1)+                              unpackTo (val :: acc) +                                       (assert_smaller loc (loc - 1))++||| Create a new buffer, copying the contents of the old buffer to the new.+||| Returns 'Nothing' if resizing fails+export+resizeBuffer : Buffer -> Int -> IO (Maybe Buffer)+resizeBuffer old newsize+    = do Just buf <- newBuffer newsize+              | Nothing => pure Nothing+         -- If the new buffer is smaller than the old one, just copy what+         -- fits+         let oldsize = size old+         let len = if newsize < oldsize then newsize else oldsize+         copyData old 0 len buf 0+         pure (Just buf)
libs/base/base.ipkg view
@@ -21,7 +21,7 @@           Data.Nat.Views,           Data.Primitives.Views,           Data.String.Views,-          Data.So, Data.String,+          Data.So, Data.String, Data.Buffer,            Control.Isomorphism,           Control.Monad.Identity,
libs/contrib/Control/ST.idr view
@@ -11,65 +11,65 @@ data Resource : Type where      MkRes : label -> Type -> Resource +export+data Var = MkVar -- Phantom, just for labelling purposes+ %error_reverse public export-(:::) : label -> Type -> Resource+(:::) : Var -> Type -> Resource (:::) = MkRes -export-data Var = MkVar -- Phantom, just for labelling purposes- {- Contexts for holding current resources states -}-namespace Context+namespace Resources   public export-  data Context : Type where-       Nil : Context-       (::) : Resource -> Context -> Context+  data Resources : Type where+       Nil : Resources+       (::) : Resource -> Resources -> Resources    public export-  (++) : Context -> Context -> Context+  (++) : Resources -> Resources -> Resources   (++) [] ys = ys   (++) (x :: xs) ys = x :: xs ++ ys  {- Proof that a label has a particular type in a given context -} public export-data InState : lbl -> Type -> Context -> Type where+data InState : Var -> Type -> Resources -> Type where      Here : InState lbl st (MkRes lbl st :: rs)      There : InState lbl st rs -> InState lbl st (r :: rs)  {- Update an entry in a context with a new state -} public export-updateCtxt : (ctxt : Context) -> -             InState lbl st ctxt -> Type -> Context-updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)-updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty+updateRes : (res : Resources) -> +             InState lbl st res -> Type -> Resources+updateRes (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)+updateRes (r :: rs) (There x) ty = r :: updateRes rs x ty  {- Remove an entry from a context -} public export-drop : (ctxt : Context) -> (prf : InState lbl st ctxt) -> -       Context+drop : (res : Resources) -> (prf : InState lbl st res) -> +       Resources drop (MkRes lbl st :: rs) Here = rs drop (r :: rs) (There p) = r :: drop rs p  {- Proof that a resource state (label/type) is in a context -} public export-data ElemCtxt : Resource -> Context -> Type where-     HereCtxt : ElemCtxt a (a :: as)-     ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)+data ElemRes : Resource -> Resources -> Type where+     HereRes : ElemRes a (a :: as)+     ThereRes : ElemRes a as -> ElemRes a (b :: as)  public export %error_reduce-dropEl : (ys: _) -> ElemCtxt x ys -> Context-dropEl (x :: as) HereCtxt = as-dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p+dropEl : (ys: _) -> ElemRes x ys -> Resources+dropEl (x :: as) HereRes = as+dropEl (x :: as) (ThereRes p) = x :: dropEl as p  {- Proof that a variable name is in a context -} public export-data VarInCtxt : Var -> Context -> Type where-     VarHere   : VarInCtxt a (MkRes a st :: as)-     VarThere  : VarInCtxt a as -> VarInCtxt a (b :: as)+data VarInRes : Var -> Resources -> Type where+     VarHere   : VarInRes a (MkRes a st :: as)+     VarThere  : VarInRes a as -> VarInRes a (b :: as)  public export %error_reduce-dropVarIn : (ys: _) -> VarInCtxt x ys -> Context+dropVarIn : (ys: _) -> VarInRes x ys -> Resources dropVarIn ((MkRes x _) :: as) VarHere = as dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p @@ -85,130 +85,134 @@        (::) : Var -> VarList ts -> VarList (t :: ts)    public export-  mkCtxt : VarList tys -> Context-  mkCtxt [] = []-  mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs+  mkRes : VarList tys -> Resources+  mkRes [] = []+  mkRes {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkRes vs -{- Proof that a context is a subset of another context -}+{- Proof that a list of resources is a subset of another list -} public export-data SubCtxt : Context -> Context -> Type where-     SubNil : SubCtxt [] []-     InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->-              SubCtxt (x :: xs) ys-     Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)+data SubRes : Resources -> Resources -> Type where+     SubNil : SubRes [] []+     Skip : SubRes xs ys -> SubRes xs (y :: ys)+     InRes : (el : ElemRes x ys) -> SubRes xs (dropEl ys el) ->+              SubRes (x :: xs) ys  %hint public export-subCtxtId : SubCtxt xs xs-subCtxtId {xs = []} = SubNil-subCtxtId {xs = (x :: xs)} = InCtxt HereCtxt subCtxtId+subResId : SubRes xs xs+subResId {xs = []} = SubNil+subResId {xs = (x :: xs)} = InRes HereRes subResId  public export-subCtxtNil : SubCtxt [] xs-subCtxtNil {xs = []} = SubNil-subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil+subResNil : SubRes [] xs+subResNil {xs = []} = SubNil+subResNil {xs = (x :: xs)} = Skip subResNil  {- Proof that every variable in the list appears once in the context -} public export-data VarsIn : List Var -> Context -> Type where+data VarsIn : List Var -> Resources -> Type where      VarsNil : VarsIn [] []-     InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->-                 VarsIn (x :: xs) ys      SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)+     InResVar : (el : VarInRes x ys) -> VarsIn xs (dropVarIn ys el) ->+                 VarsIn (x :: xs) ys  public export-Uninhabited (ElemCtxt x []) where-  uninhabited HereCtxt impossible-  uninhabited (ThereCtxt _) impossible+Uninhabited (ElemRes x []) where+  uninhabited HereRes impossible+  uninhabited (ThereRes _) impossible  public export %error_reduce-updateWith : (new : Context) -> (xs : Context) ->-             SubCtxt ys xs -> Context+updateWith : (new : Resources) -> (xs : Resources) ->+             SubRes ys xs -> Resources -- At the end, add the ones which were updated by the subctxt updateWith new [] SubNil = new-updateWith new [] (InCtxt el z) = absurd el+updateWith new [] (InRes el z) = absurd el -- Don't add the ones which were consumed by the subctxt-updateWith [] (x :: xs) (InCtxt el p) +updateWith [] (x :: xs) (InRes el p)      = updateWith [] (dropEl _ el) p-updateWith (n :: ns) (x :: xs) (InCtxt el p) +-- A new item corresponding to an existing thing+updateWith (n :: ns) (x :: xs) (InRes el p)      = n :: updateWith ns (dropEl _ el) p--- Do add the ones we didn't use in the subctxt updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p  public export-getVarType : (xs : Context) -> VarInCtxt v xs -> Type+getVarType : (xs : Resources) -> VarInRes v xs -> Type getVarType ((MkRes v st) :: as) VarHere = st getVarType (b :: as) (VarThere x) = getVarType as x  public export getCombineType : VarsIn ys xs -> List Type getCombineType VarsNil = []-getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y+getCombineType (InResVar el y) = getVarType _ el :: getCombineType y getCombineType (SkipVar x) = getCombineType x  public export-dropCombined : VarsIn vs ctxt -> Context-dropCombined {ctxt = []} VarsNil = []-dropCombined {ctxt} (InCtxtVar el y) = dropCombined y-dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x+dropCombined : VarsIn vs res -> Resources+dropCombined {res = []} VarsNil = []+dropCombined {res} (InResVar el y) = dropCombined y+dropCombined {res = (y :: ys)} (SkipVar x) = y :: dropCombined x  public export-combineVarsIn : (ctxt : Context) -> VarsIn (comp :: vs) ctxt -> Context-combineVarsIn {comp} ctxt (InCtxtVar el x) -     = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))+combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources+combineVarsIn {comp} res (InResVar el x) +     = ((comp ::: Composite (getCombineType x)) :: dropCombined (InResVar el x)) combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x  namespace Env   public export-  data Env : Context -> Type where+  data Env : Resources -> Type where        Nil : Env []        (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs) -lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty+  (++) : Env xs -> Env ys -> Env (xs ++ ys)+  (++) [] ys = ys+  (++) (x :: xs) ys = x :: xs ++ ys++lookupEnv : InState lbl ty res -> Env res -> ty lookupEnv Here (x :: xs) = x lookupEnv (There p) (x :: xs) = lookupEnv p xs -updateEnv : (prf : InState lbl ty ctxt) -> Env ctxt -> ty' -> -            Env (updateCtxt ctxt prf ty')+updateEnv : (prf : InState lbl ty res) -> Env res -> ty' -> +            Env (updateRes res prf ty') updateEnv Here (x :: xs) val = val :: xs updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val -dropVal : (prf : InState lbl st ctxt) -> Env ctxt -> Env (drop ctxt prf)+dropVal : (prf : InState lbl st res) -> Env res -> Env (drop res prf) dropVal Here (x :: xs) = xs dropVal (There p) (x :: xs) = x :: dropVal p xs -envElem : ElemCtxt x xs -> Env xs -> Env [x]-envElem HereCtxt (x :: xs) = [x]-envElem (ThereCtxt p) (x :: xs) = envElem p xs+envElem : ElemRes x xs -> Env xs -> Env [x]+envElem HereRes (x :: xs) = [x]+envElem (ThereRes p) (x :: xs) = envElem p xs -dropDups : Env xs -> (el : ElemCtxt x xs) -> Env (dropEl xs el)-dropDups (y :: ys) HereCtxt = ys-dropDups (y :: ys) (ThereCtxt p) = y :: dropDups ys p+dropDups : Env xs -> (el : ElemRes x xs) -> Env (dropEl xs el)+dropDups (y :: ys) HereRes = ys+dropDups (y :: ys) (ThereRes p) = y :: dropDups ys p  -dropEntry : Env ctxt -> (prf : VarInCtxt x ctxt) -> Env (dropVarIn ctxt prf)+dropEntry : Env res -> (prf : VarInRes x res) -> Env (dropVarIn res prf) dropEntry (x :: env) VarHere = env dropEntry (x :: env) (VarThere y) = x :: dropEntry env y -dropVarsIn : Env ctxt -> (prf : VarsIn vs ctxt) -> Env (dropCombined prf)+dropVarsIn : Env res -> (prf : VarsIn vs res) -> Env (dropCombined prf) dropVarsIn [] VarsNil = []-dropVarsIn env (InCtxtVar el z) = dropVarsIn (dropEntry env el) z+dropVarsIn env (InResVar el z) = dropVarsIn (dropEntry env el) z dropVarsIn (x :: env) (SkipVar z) = x :: dropVarsIn env z -getVarEntry : Env ctxt -> (prf : VarInCtxt v ctxt) -> getVarType ctxt prf+getVarEntry : Env res -> (prf : VarInRes v res) -> getVarType res prf getVarEntry (x :: xs) VarHere = x getVarEntry (x :: env) (VarThere p) = getVarEntry env p -mkComposite : Env ctxt -> (prf : VarsIn vs ctxt) -> Composite (getCombineType prf)+mkComposite : Env res -> (prf : VarsIn vs res) -> Composite (getCombineType prf) mkComposite [] VarsNil = CompNil-mkComposite env (InCtxtVar el z) +mkComposite env (InResVar el z)      = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z) mkComposite (x :: env) (SkipVar z) = mkComposite env z -rebuildVarsIn : Env ctxt -> (prf : VarsIn (comp :: vs) ctxt) -> -                Env (combineVarsIn ctxt prf)-rebuildVarsIn env (InCtxtVar el p) -     = mkComposite (dropEntry env el) p :: dropVarsIn env (InCtxtVar el p)+rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) -> +                Env (combineVarsIn res prf)+rebuildVarsIn env (InResVar el p) +     = mkComposite (dropEntry env el) p :: dropVarsIn env (InResVar el p) rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p  {- Some things to make STrans interfaces look prettier -}@@ -217,14 +221,14 @@            public export data Action : Type -> Type where-     Stable : lbl -> Type -> Action ty-     Trans : lbl -> Type -> (ty -> Type) -> Action ty-     Remove : lbl -> Type -> Action ty-     Add : (ty -> Context) -> Action ty+     Stable : Var -> Type -> Action ty+     Trans : Var -> Type -> (ty -> Type) -> Action ty+     Remove : Var -> Type -> Action ty+     Add : (ty -> Resources) -> Action ty  namespace Stable   public export %error_reduce-  (:::) : lbl -> Type -> Action ty+  (:::) : Var -> Type -> Action ty   (:::) = Stable  namespace Trans@@ -232,7 +236,7 @@   data Trans ty = (:->) Type Type    public export %error_reduce-  (:::) : lbl -> Trans ty -> Action ty+  (:::) : Var -> Trans ty -> Action ty   (:::) lbl (st :-> st') = Trans lbl st (const st')  namespace DepTrans@@ -240,29 +244,33 @@   data DepTrans ty = (:->) Type (ty -> Type)    public export %error_reduce-  (:::) : lbl -> DepTrans ty -> Action ty+  (:::) : Var -> DepTrans ty -> Action ty   (:::) lbl (st :-> st') = Trans lbl st st'  public export or : a -> a -> Either b c -> a or x y = either (const x) (const y) -public export-add : Type -> Action a+public export %error_reduce+add : Type -> Action Var add ty = Add (\var => [var ::: ty])+ +public export %error_reduce+remove : Var -> Type -> Action ty+remove = Remove -public export-addIfRight : Type -> Action (Either a b)+public export %error_reduce+addIfRight : Type -> Action (Either a Var) addIfRight ty = Add (either (const []) (\var => [var ::: ty])) -public export-addIfJust : Type -> Action (Maybe a)+public export %error_reduce+addIfJust : Type -> Action (Maybe Var) addIfJust ty = Add (maybe [] (\var => [var ::: ty]))  public export-kept : SubCtxt xs ys -> Context+kept : SubRes xs ys -> Resources kept SubNil = []-kept (InCtxt el p) = kept p+kept (InRes el p) = kept p kept (Skip {y} p) = y :: kept p  -- We can only use new/delete/read/write on things wrapped in State. Only an@@ -275,7 +283,7 @@ export data STrans : (m : Type -> Type) ->               (ty : Type) ->-              Context -> (ty -> Context) ->+              Resources -> (ty -> Resources) ->               Type where      Pure : (result : ty) ->              STrans m ty (out_fn result) out_fn@@ -283,59 +291,73 @@             ((result : a) ->                  STrans m b (st2_fn result) st3_fn) ->             STrans m b st1 st3_fn-     Lift : Monad m => m t -> STrans m t ctxt (const ctxt)+     Lift : Monad m => m t -> STrans m t res (const res)+     RunAs : Applicative m => STrans m t in_res (const out_res) -> +             STrans m (m t) in_res (const out_res)       New : (val : state) -> -           STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)+           STrans m Var res (\lbl => (lbl ::: state) :: res)      Delete : (lbl : Var) ->-              (prf : InState lbl st ctxt) ->-              STrans m () ctxt (const (drop ctxt prf))-     DropSubCtxt : (prf : SubCtxt ys xs) ->-                   STrans m (Env ys) xs (const (kept prf))+              (prf : InState lbl st res) ->+              STrans m () res (const (drop res prf))+     DropSubRes : (prf : SubRes ys xs) ->+                  STrans m (Env ys) xs (const (kept prf))       Split : (lbl : Var) ->-             (prf : InState lbl (Composite vars) ctxt) ->-             STrans m (VarList vars) ctxt -                   (\ vs => mkCtxt vs ++ -                            updateCtxt ctxt prf (State ()))+             (prf : InState lbl (Composite vars) res) ->+             STrans m (VarList vars) res +                   (\ vs => mkRes vs ++ +                            updateRes res prf (State ()))      Combine : (comp : Var) -> (vs : List Var) ->-               (prf : VarsIn (comp :: vs) ctxt) ->-               STrans m () ctxt-                   (const (combineVarsIn ctxt prf))+               (prf : VarsIn (comp :: vs) res) ->+               STrans m () res+                   (const (combineVarsIn res prf))+     ToEnd : (lbl : Var) ->+             (prf : InState lbl state res) ->+             STrans m () res (const (drop res prf ++ [lbl ::: state])) -     Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->-            STrans m t old (\res => updateWith (new_f res) old ctxt_prf)+     Call : STrans m t sub new_f -> (res_prf : SubRes sub old) ->+            STrans m t old (\res => updateWith (new_f res) old res_prf)       Read : (lbl : Var) ->-            (prf : InState lbl ty ctxt) ->-            STrans m ty ctxt (const ctxt)+            (prf : InState lbl ty res) ->+            STrans m ty res (const res)      Write : (lbl : Var) ->-             (prf : InState lbl ty ctxt) ->+             (prf : InState lbl ty res) ->              (val : ty') ->-             STrans m () ctxt (const (updateCtxt ctxt prf ty'))+             STrans m () res (const (updateRes res prf ty')) +namespace Loop+  export+  data STransLoop : (m : Type -> Type) -> (ty : Type) ->+                    Resources -> (ty -> Resources) -> Type where+       Bind : STrans m a st1 st2_fn ->+              ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->+              STransLoop m b st1 st3_fn+       Pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn+ export-dropEnv : Env ys -> SubCtxt xs ys -> Env xs+dropEnv : Env ys -> SubRes xs ys -> Env xs dropEnv [] SubNil = []-dropEnv [] (InCtxt idx rest) = absurd idx-dropEnv (z :: zs) (InCtxt idx rest) +dropEnv [] (InRes idx rest) = absurd idx+dropEnv (z :: zs) (InRes idx rest)      = let [e] = envElem idx (z :: zs) in           e :: dropEnv (dropDups (z :: zs) idx) rest dropEnv (z :: zs) (Skip p) = dropEnv zs p -keepEnv : Env ys -> (prf : SubCtxt xs ys) -> Env (kept prf)+keepEnv : Env ys -> (prf : SubRes xs ys) -> Env (kept prf) keepEnv env SubNil = env-keepEnv env (InCtxt el prf) = keepEnv (dropDups env el) prf+keepEnv env (InRes el prf) = keepEnv (dropDups env el) prf keepEnv (z :: zs) (Skip prf) = z :: keepEnv zs prf  -- Corresponds pretty much exactly to 'updateWith'-rebuildEnv : Env new -> Env old -> (prf : SubCtxt sub old) ->+rebuildEnv : Env new -> Env old -> (prf : SubRes sub old) ->              Env (updateWith new old prf) rebuildEnv new [] SubNil = new-rebuildEnv new [] (InCtxt el p) = absurd el-rebuildEnv [] (x :: xs) (InCtxt el p) +rebuildEnv new [] (InRes el p) = absurd el+rebuildEnv [] (x :: xs) (InRes el p)      = rebuildEnv [] (dropDups (x :: xs) el) p-rebuildEnv (e :: es) (x :: xs) (InCtxt el p) +rebuildEnv (e :: es) (x :: xs) (InRes el p)      = e :: rebuildEnv es (dropDups (x :: xs) el) p rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p @@ -347,9 +369,10 @@ runST env (Lift action) k     = do res <- action         k res env+runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env') runST env (New val) k = k MkVar (val :: env) runST env (Delete lbl prf) k = k () (dropVal prf env)-runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)+runST env (DropSubRes prf) k = k (dropEnv env prf) (keepEnv env prf) runST env (Split lbl prf) k = let val = lookupEnv prf env                                    env' = updateEnv prf env (Value ()) in                                   k (mkVars val) (addToEnv val env')@@ -358,22 +381,37 @@     mkVars CompNil = []     mkVars (CompCons x xs) = MkVar :: mkVars xs -    addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)+    addToEnv : (comp : Composite ts) -> Env xs -> Env (mkRes (mkVars comp) ++ xs)     addToEnv CompNil env = env     addToEnv (CompCons x xs) env = x :: addToEnv xs env+runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env]) runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)-runST env (Call prog ctxt_prf) k -   = let env' = dropEnv env ctxt_prf in+runST env (Call prog res_prf) k +   = let env' = dropEnv env res_prf in          runST env' prog-                 (\prog', envk => k prog' (rebuildEnv envk env ctxt_prf))+                 (\prog', envk => k prog' (rebuildEnv envk env res_prf)) runST env (Read lbl prf) k = k (lookupEnv prf env) env runST env (Write lbl prf val) k = k () (updateEnv prf env val) +export+data Fuel = Empty | More (Lazy Fuel) +export partial+forever : Fuel+forever = More forever++runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->+            (k : (x : a) -> Env (outfn x) -> m b) ->+            (onDry : m b) -> m b+runSTLoop Empty _ _ _ onDry = onDry+runSTLoop (More x) env (Bind prog next) k onDry +    = runST env prog (\prog', env' => runSTLoop x env' (next prog') k onDry)+runSTLoop (More x) env (Pure result) k onDry = k result env+ export  pure : (result : ty) -> STrans m ty (out_fn result) out_fn pure = Pure- + export  (>>=) : STrans m a st1 st2_fn ->         ((result : a) -> STrans m b (st2_fn result) st3_fn) ->@@ -381,65 +419,102 @@ (>>=) = Bind  export-lift : Monad m => m t -> STrans m t ctxt (const ctxt)+returning : (result : ty) -> STrans m () res (const (out_fn result)) ->+            STrans m ty res out_fn+returning res prog = do prog+                        pure res+ ++export+lift : Monad m => m t -> STrans m t res (const res) lift = Lift  export+runAs : Applicative m => STrans m t in_res (const out_res) -> +        STrans m (m t) in_res (const out_res)+runAs = RunAs++export new : (val : state) -> -      STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)+      STrans m Var res (\lbl => (lbl ::: State state) :: res) new val = New (Value val)  export delete : (lbl : Var) ->-         {auto prf : InState lbl (State st) ctxt} ->-         STrans m () ctxt (const (drop ctxt prf))+         {auto prf : InState lbl (State st) res} ->+         STrans m () res (const (drop res prf)) delete lbl {prf} = Delete lbl prf  -- Keep only a subset of the current set of resources. Returns the -- environment corresponding to the dropped portion. export-dropSubCtxt : {auto prf : SubCtxt ys xs} ->-              STrans m (Env ys) xs (const (kept prf))-dropSubCtxt {prf} = DropSubCtxt prf+dropSub : {auto prf : SubRes ys xs} ->+          STrans m (Env ys) xs (const (kept prf))+dropSub {prf} = DropSubRes prf  export split : (lbl : Var) ->-        {auto prf : InState lbl (Composite vars) ctxt} ->-        STrans m (VarList vars) ctxt -              (\ vs => mkCtxt vs ++ -                       updateCtxt ctxt prf (State ()))+        {auto prf : InState lbl (Composite vars) res} ->+        STrans m (VarList vars) res +              (\ vs => mkRes vs ++ +                       updateRes res prf (State ())) split lbl {prf} = Split lbl prf  export combine : (comp : Var) -> (vs : List Var) ->-          {auto prf : InState comp (State ()) ctxt} ->-          {auto var_prf : VarsIn (comp :: vs) ctxt} ->-          STrans m () ctxt-              (const (combineVarsIn ctxt var_prf))+          {auto prf : InState comp (State ()) res} ->+          {auto var_prf : VarsIn (comp :: vs) res} ->+          STrans m () res+              (const (combineVarsIn res var_prf)) combine comp vs {var_prf} = Combine comp vs var_prf+     +export+toEnd : (lbl : Var) ->+        {auto prf : InState lbl state res} ->+        STrans m () res (const (drop res prf ++ [lbl ::: state]))+toEnd lbl {prf} = ToEnd lbl prf  export -- implicit ??? call : STrans m t sub new_f ->-       {auto ctxt_prf : SubCtxt sub old} ->-       STrans m t old (\res => updateWith (new_f res) old ctxt_prf)-call prog {ctxt_prf} = Call prog ctxt_prf+       {auto res_prf : SubRes sub old} ->+       STrans m t old (\res => updateWith (new_f res) old res_prf)+call prog {res_prf} = Call prog res_prf   export read : (lbl : Var) ->-       {auto prf : InState lbl (State ty) ctxt} ->-       STrans m ty ctxt (const ctxt)+       {auto prf : InState lbl (State ty) res} ->+       STrans m ty res (const res) read lbl {prf} = do Value x <- Read lbl prf                     pure x  export write : (lbl : Var) ->-        {auto prf : InState lbl ty ctxt} ->+        {auto prf : InState lbl ty res} ->         (val : ty') ->-        STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))+        STrans m () res (const (updateRes res prf (State ty'))) write lbl {prf} val = Write lbl prf (Value val)+       +export+update : (lbl : Var) ->+         {auto prf : InState lbl (State ty) res} ->+         (ty -> ty') ->+         STrans m () res (const (updateRes res prf (State ty')))+update lbl f = do x <- read lbl+                  write lbl (f x)++namespace Loop+   export+   (>>=) : STrans m a st1 st2_fn ->+          ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->+          STransLoop m b st1 st3_fn+   (>>=) = Bind++   export+   pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn+   pure = Pure      public export %error_reduce-out_res : ty -> (as : List (Action ty)) -> Context+out_res : ty -> (as : List (Action ty)) -> Resources out_res x [] = [] out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs out_res x ((Trans lbl inr outr) :: xs) @@ -448,7 +523,7 @@ out_res x (Add outf :: xs) = outf x ++ out_res x xs  public export %error_reduce-in_res : (as : List (Action ty)) -> Context+in_res : (as : List (Action ty)) -> Resources in_res [] = [] in_res ((Stable lbl inr) :: xs) = (lbl ::: inr) :: in_res xs in_res ((Trans lbl inr outr) :: xs) = (lbl ::: inr) :: in_res xs@@ -462,6 +537,13 @@      List (Action ty) -> Type ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs) +public export+%error_reduce -- always evaluate this before showing errors+STLoop : (m : Type -> Type) ->+         (ty : Type) -> +         List (Action ty) -> Type+STLoop m ty xs = STransLoop m ty (in_res xs) (\result : ty => out_res result xs)+ -- Console IO is useful sufficiently often that let's have it here public export interface ConsoleIO (m : Type -> Type) where@@ -469,6 +551,10 @@   getStr : STrans m String xs (const xs)  export+putStrLn : ConsoleIO m => String -> STrans m () xs (const xs)+putStrLn str = putStr (str ++ "\n")++export ConsoleIO IO where   putStr str = lift (Interactive.putStr str)   getStr = lift Interactive.getLine@@ -478,20 +564,35 @@ run : Applicative m => ST m a [] -> m a run prog = runST [] prog (\res, env' => pure res) +export+runLoop : Applicative m => Fuel -> STLoop m a [] -> +          (onEmpty : m a) ->+          m a+runLoop fuel prog onEmpty+    = runSTLoop fuel [] prog (\res, env' => pure res) onEmpty+ ||| runWith allows running an STrans program with an initial environment, ||| which must be consumed. ||| It's only allowed in the IO monad, because it's inherently unsafe, so-||| we don't want to be able to use it under a 'lift in just *any* ST program -+||| we don't want to be able to use it under a 'lift' in just *any* ST program - ||| if we have access to an 'Env' we can easily duplicate it - so it's the ||| responsibility of an implementation of an interface in IO which uses it ||| to ensure that it isn't duplicated. export-runWith : {ctxtf : _} ->-          Env ctxt -> STrans IO a ctxt (\res => ctxtf res) -> -          IO (res ** Env (ctxtf res))+runWith : {resf : _} ->+          Env res -> STrans IO a res (\result => resf result) -> +          IO (result ** Env (resf result)) runWith env prog = runST env prog (\res, env' => pure (res ** env'))  export+runWithLoop : {resf : _} ->+          Env res -> Fuel -> STransLoop IO a res (\result => resf result) -> +          IO (Maybe (result ** Env (resf result)))+runWithLoop env fuel prog +    = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env'))) +                              (pure Nothing)++export runPure : ST Basics.id a [] -> a runPure prog = runST [] prog (\res, env' => res) @@ -500,7 +601,7 @@ %error_handler export st_precondition : Err -> Maybe (List ErrorReportPart)-st_precondition (CantSolveGoal `(SubCtxt ~sub ~all) _)+st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)    = pure        [TextPart "'call' is not valid here. ",        TextPart "The operation has preconditions ",@@ -519,10 +620,12 @@   where     getPreconditions : TT -> Maybe TT     getPreconditions `(STrans ~m ~ret ~pre ~post) = Just pre+    getPreconditions `(STransLoop ~m ~ret ~pre ~post) = Just pre     getPreconditions _ = Nothing      getPostconditions : TT -> Maybe TT     getPostconditions `(STrans ~m ~ret ~pre ~post) = Just post+    getPostconditions `(STransLoop ~m ~ret ~pre ~post) = Just post     getPostconditions _ = Nothing      renderPre : TT -> TT -> List (ErrorReportPart)
+ libs/contrib/Control/ST/Exception.idr view
@@ -0,0 +1,38 @@+module Control.ST.Exception++import Control.ST+import Control.Catchable+import Control.IOExcept++public export+interface Exception (m : Type -> Type) errorType | m where+    throw : errorType -> STrans m a ctxt (const ctxt)++    catch : STrans m a in_res (const out_res) ->+            (errorType -> STrans m a out_res (const out_res)) ->+            STrans m a in_res (const out_res)++export+Exception (Either errorType) errorType where+    throw err = lift (Left err)+    catch prog f = do res <- runAs prog+                      case res of+                           Left err => f err+                           Right ok => pure ok++export+Exception Maybe () where+    throw err = lift Nothing+    catch prog f = do res <- runAs prog+                      case res of+                           Nothing => f ()+                           Just ok => pure ok++export+Exception (IOExcept errorType) errorType where+    throw err = lift (ioe_fail err)+    catch prog f = do io_res <- runAs prog+                      res <- lift (catch (do r <- io_res+                                             pure (Right r))+                                         (\err => pure (Left err)))+                      either (\err => f err) (\ok => pure ok) res
libs/contrib/Control/ST/ImplicitCall.idr view
@@ -7,7 +7,7 @@ ||| potentially more difficult to read. export implicit imp_call : STrans m t ys ys' ->-       {auto ctxt_prf : SubCtxt ys xs} ->-       STrans m t xs (\res => updateWith (ys' res) xs ctxt_prf)+           {auto res_prf : SubRes ys xs} ->+           STrans m t xs (\res => updateWith (ys' res) xs res_prf) imp_call = call
libs/contrib/contrib.ipkg view
@@ -8,7 +8,7 @@           Control.Algebra.NumericImplementations,           Control.Isomorphism.Primitives,           Control.Partial,-          Control.ST, Control.ST.ImplicitCall,+          Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,            Interfaces.Verified,
libs/prelude/Builtins.idr view
@@ -210,6 +210,7 @@ export data CData : Type  %extern prim__readFile : prim__WorldType -> Ptr -> String+%extern prim__readChars : prim__WorldType -> Int -> Ptr -> String %extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int  %extern prim__vm : prim__WorldType -> Ptr
libs/prelude/IO.idr view
@@ -134,6 +134,10 @@ prim_fread : Ptr -> IO' l String prim_fread h = MkIO (\w => prim_io_pure (prim__readFile (world w) h)) +prim_freadChars : Int -> Ptr -> IO' l String+prim_freadChars len h +     = MkIO (\w => prim_io_pure (prim__readChars (world w) len h))+ prim_fwrite : Ptr -> String -> IO' l Int prim_fwrite h s    = MkIO (\w => prim_io_pure (prim__writeFile (world w) h s))
libs/prelude/Prelude/Bits.idr view
@@ -2,12 +2,14 @@  import Builtins +import Prelude.Algebra import Prelude.Basics import Prelude.Bool import Prelude.Cast import Prelude.Chars import Prelude.Interfaces import Prelude.Foldable+import Prelude.Functor import Prelude.Nat import Prelude.List import Prelude.Strings@@ -15,8 +17,54 @@ %access public export %default total -b8ToString : Bits8 -> String-b8ToString c = pack (with List [c1, c2])+--------------------------------------------------------------------------------+-- Convert to `List Bits8`+--------------------------------------------------------------------------------++||| Convert to list of `Bits8` with the most signficant byte at the+||| head.+b8ToBytes : Bits8 -> List Bits8+b8ToBytes b = [b]++||| Convert to list of `Bits8` with the most signficant byte at the+||| head.+b16ToBytes : Bits16 -> List Bits8+b16ToBytes b =+  [ prim__truncB16_B8 (prim__lshrB16 b 8)+  , prim__truncB16_B8 b+  ]++||| Convert to list of `Bits8` with the most signficant byte at the+||| head.+b32ToBytes : Bits32 -> List Bits8+b32ToBytes b =+  [ prim__truncB32_B8 (prim__lshrB32 b 24)+  , prim__truncB32_B8 (prim__lshrB32 b 16)+  , prim__truncB32_B8 (prim__lshrB32 b 8)+  , prim__truncB32_B8 b+  ]++||| Convert to list of `Bits8` with the most signficant byte at the+||| head.+b64ToBytes : Bits64 -> List Bits8+b64ToBytes b =+  [ prim__truncB64_B8 (prim__lshrB64 b 56)+  , prim__truncB64_B8 (prim__lshrB64 b 48)+  , prim__truncB64_B8 (prim__lshrB64 b 40)+  , prim__truncB64_B8 (prim__lshrB64 b 32)+  , prim__truncB64_B8 (prim__lshrB64 b 24)+  , prim__truncB64_B8 (prim__lshrB64 b 16)+  , prim__truncB64_B8 (prim__lshrB64 b 8)+  , prim__truncB64_B8 b+  ]++--------------------------------------------------------------------------------+-- Hex Strings+--------------------------------------------------------------------------------++||| Encode `Bits8` as a 2-character hex string.+b8ToHexString : Bits8 -> String+b8ToHexString c = pack [c1, c2]   where getDigit : Bits8 -> Char         getDigit b = let n = prim__zextB8_Int b in                      if n >= 0 && n <= 9@@ -27,30 +75,64 @@         c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)         c2 = getDigit (prim__andB8 c 15) +||| Encode `Bits16` as a 4-character hex string.+b16ToHexString : Bits16 -> String+b16ToHexString c = concatMap b8ToHexString (b16ToBytes c) +||| Encode `Bits32` as an 8-character hex string.+b32ToHexString : Bits32 -> String+b32ToHexString c = concatMap b8ToHexString (b32ToBytes c)++||| Encode `Bits64` as a 16-character hex string.+b64ToHexString : Bits64 -> String+b64ToHexString c = concatMap b8ToHexString (b64ToBytes c)+++--------------------------------------------------------------------------------+-- Binary Strings+--------------------------------------------------------------------------------++||| Encode `Bits8` as an 8-character binary string.+b8ToBinString : Bits8 -> String+b8ToBinString b = pack $ map (bitChar b) [7,6,5,4,3,2,1,0]+  where bitChar : Bits8 -> Bits8 -> Char+        bitChar b i = case b `prim__andB8` (1 `prim__shlB8` i) of+                           0 => '0'+                           _ => '1'++||| Encode `Bits16` as a 16-character binary string.+b16ToBinString : Bits16 -> String+b16ToBinString c = concatMap b8ToBinString (b16ToBytes c)++||| Encode `Bits32` as a 32-character binary string.+b32ToBinString : Bits32 -> String+b32ToBinString c = concatMap b8ToBinString (b32ToBytes c)++||| Encode `Bits64` as a 64-character binary string.+b64ToBinString : Bits64 -> String+b64ToBinString c = concatMap b8ToBinString (b64ToBytes c)+++--------------------------------------------------------------------------------+-- Deprecated String Functions+--------------------------------------------------------------------------------++||| Encode `Bits8` as a 2-character hex string.+b8ToString : Bits8 -> String+b8ToString = b8ToHexString+%deprecate b8ToString "Please use `b8ToHexString` instead."++||| Encode `Bits16` as a 4-character hex string. b16ToString : Bits16 -> String-b16ToString c = c1 ++ c2 where-  c1 = b8ToString upper where-    upper : Bits8-    upper = prim__truncB16_B8 (prim__lshrB16 c 8)-  c2 = b8ToString lower where-    lower : Bits8-    lower = prim__truncB16_B8 c+b16ToString = b16ToHexString+%deprecate b16ToString "Please use `b16ToHexString` instead." +||| Encode `Bits32` as a 8-character hex string. b32ToString : Bits32 -> String-b32ToString c = c1 ++ c2 where-  c1 = b16ToString upper where-    upper : Bits16-    upper = prim__truncB32_B16 (prim__andB32 (prim__lshrB32 c 16) 0x0000ffff)-  c2 = b16ToString lower where-    lower : Bits16-    lower = prim__truncB32_B16 c+b32ToString = b32ToHexString+%deprecate b32ToString "Please use `b32ToHexString` instead." +||| Encode `Bits64` as a 16-character hex string. b64ToString : Bits64 -> String-b64ToString c = c1 ++ c2 where-  c1 = b32ToString upper where-    upper : Bits32-    upper = prim__truncB64_B32 (prim__andB64 (prim__lshrB64 c 32) 0x00000000ffffffff)-  c2 = b32ToString lower where-    lower : Bits32-    lower = prim__truncB64_B32 c+b64ToString = b64ToHexString+%deprecate b64ToString "Please use `b64ToHexString` instead."
libs/prelude/Prelude/File.idr view
@@ -156,6 +156,10 @@ do_fread : Ptr -> IO' l String do_fread h = prim_fread h +private+do_freadChars : Ptr -> Int -> IO' l String+do_freadChars h len = prim_freadChars len h+ export fgetc : File -> IO (Either FileError Char) fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)@@ -199,6 +203,15 @@ fGetLine : (h : File) -> IO (Either FileError String) fGetLine = fread +||| Read up to a number of characters from a file+||| @h a file handle which must be open for reading+export+fGetChars : (h : File) -> (len : Int) -> IO (Either FileError String)+fGetChars (FHandle h) len = do str <- do_freadChars h len+                               if !(ferror (FHandle h))+                                  then pure (Left FileReadError)+                                  else pure (Right str)+ %deprecate fread "Use fGetLine instead"  private@@ -251,10 +264,12 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h                        pure (p > 0) -||| Read the contents of a file into a string+||| Read the contents of a text 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.+||| This only works reliably with text files, since it relies on null-terminated+||| strings internally. ||| Returns an error if filepath is not a normal file. export readFile : (filepath : String) -> IO (Either FileError String)@@ -262,19 +277,22 @@                     | Left err => pure (Left err)                  Right max <- fileSize h                     | Left err => pure (Left err)-                 c <- readFile' h max ""+                 sb <- newStringBuffer (max + 1)+                 c <- readFile' h max sb                  closeFile h                  pure c   where-    readFile' : File -> Int -> String -> IO (Either FileError String)+    readFile' : File -> Int -> StringBuffer -> IO (Either FileError String)     readFile' h max contents =        do x <- fEOF h           if not x && max > 0-                   then do Right l <- fGetLine h+                   then do Right l <- fGetChars h 1024000                                | Left err => pure (Left err)+                           addToStringBuffer contents l                            assert_total $-                             readFile' h (max - cast (length l)) (contents ++ l)-                   else pure (Right contents)+                             readFile' h (max - 1024000) contents+                   else do str <- getStringFromBuffer contents+                           pure (Right str)  ||| Write a string to a file export
libs/prelude/Prelude/Maybe.idr view
@@ -112,7 +112,7 @@   m         <+> Nothing = m   (Just m1) <+> (Just m2) = Just (m1 <+> m2) - Monoid (Maybe a) where+Monoid (Maybe a) where   neutral = Nothing  (Monoid a, Eq a) => Cast a (Maybe a) where
libs/prelude/Prelude/Nat.idr view
@@ -236,12 +236,12 @@ Cast String Nat where     cast str = cast (the Integer (cast str)) -||| A wrapper for Nat that specifies the semigroup and monad implementations that use (*)+||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*) record Multiplicative where   constructor GetMultiplicative   _ : Nat -||| A wrapper for Nat that specifies the semigroup and monad implementations that use (+)+||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (+) record Additive where   constructor GetAdditive   _ : Nat
libs/prelude/Prelude/Show.idr view
@@ -164,16 +164,16 @@   show () = "()"  Show Bits8 where-  show b = b8ToString b+  show b = b8ToHexString b  Show Bits16 where-  show b = b16ToString b+  show b = b16ToHexString b  Show Bits32 where-  show b = b32ToString b+  show b = b32ToHexString b  Show Bits64 where-  show b = b64ToString b+  show b = b64ToHexString b  (Show a, Show b) => Show (a, b) where     show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
libs/prelude/Prelude/Strings.idr view
@@ -36,6 +36,39 @@ (++) : String -> String -> String (++) = prim__concat +||| A preallocated buffer for building a String. This allows a function (in IO)+||| to allocate enough space for a stirng which will be build from smaller+||| pieces without having to allocate at every step.+||| To build a string using a `StringBuffer`, see `newStringBuffer`,+||| `addToStringBuffer` and `getStringFromBuffer`.+export+data StringBuffer = MkString Ptr++||| Create a buffer for a string with maximum length len+export+newStringBuffer : (len : Int) -> IO StringBuffer+newStringBuffer len = do ptr <- foreign FFI_C "idris_makeStringBuffer"+                                         (Int -> IO Ptr) len+                         pure (MkString ptr)++||| Append a string to the end of a string buffer+export+addToStringBuffer : StringBuffer -> String -> IO ()+addToStringBuffer (MkString ptr) str =+    foreign FFI_C "idris_addToString" (Ptr -> String -> IO ())+            ptr str++||| Get the string from a string buffer. The buffer is invalid after+||| this.+export+getStringFromBuffer : StringBuffer -> IO String+getStringFromBuffer (MkString ptr) =+    do vm <- getMyVM+       MkRaw str <- foreign FFI_C "idris_getString"+                            (Ptr -> Ptr -> IO (Raw String))+                            vm ptr+       pure str+ ||| Returns the first character in the specified string. ||| ||| Doesn't work for empty strings.
man/idris.1 view
@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "5 March 2017" "0.99.1" "Idris man page"+.TH man 1 "26 March 2017" "0.99.2" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS
rts/Makefile view
@@ -2,10 +2,10 @@  OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \        idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o mini-gmp.o \-       getline.o+       idris_buffer.o getline.o HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \        idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \-       idris_utf8.h getline.h+       idris_buffer.h idris_utf8.h getline.h CFLAGS := $(CFLAGS) CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\"" CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\""
+ rts/idris_buffer.c view
@@ -0,0 +1,86 @@+#include "idris_rts.h"+#include "idris_buffer.h"++typedef struct {+    int size;+    uint8_t* data;+} Buffer;++void* idris_newBuffer(int bytes) {+    Buffer* buf = malloc(sizeof(Buffer) + bytes*sizeof(uint8_t));+    if (buf == NULL) {+        return NULL;+    }++    buf->size = bytes;+    buf->data = (uint8_t*)(buf+1);+    memset(buf->data, 0, bytes);++    return buf;+}++void idris_copyBuffer(void* from, int start, int len,+                      void* to, int loc) {+    Buffer* bfrom = from;+    Buffer* bto = to;++    if (loc >= 0 && loc+len <= bto->size) {+        memcpy((bto->data)+loc, (bfrom->data)+start, len);+    }+}++int idris_getBufferSize(void* buffer) {+    return ((Buffer*)buffer)->size;+}++void idris_setBufferByte(void* buffer, int loc, uint8_t byte) {+    Buffer* b = buffer;+    if (loc >= 0 && loc < b->size) {+        b->data[loc] = byte;+    }+}++void idris_setBufferString(void* buffer, int loc, char* str) {+    Buffer* b = buffer;+    int len = strlen(str);++    if (loc >= 0 && loc+len <= b->size) {+        memcpy((b->data)+loc, str, len);+    }+}++uint8_t idris_getBufferByte(void* buffer, int loc) {+    Buffer* b = buffer;+    if (loc >= 0 && loc < b->size) {+        return b->data[loc];+    } else {+        return 0;+    }+}++int idris_readBuffer(FILE* h, void* buffer, int loc, int max) {+    Buffer* b = buffer;+    size_t len;++    if (loc >= 0 && loc < b->size) {+        if (loc + max > b->size) {+            max = b->size - loc;+        }+        len = fread((b->data)+loc, sizeof(uint8_t), (size_t)max, h);+        return len;+    } else {+        return 0;+    }+}++void idris_writeBuffer(FILE* h, void* buffer, int loc, int len) {+    Buffer* b = buffer;++    if (loc >= 0 && loc < b->size) {+        if (loc + len > b->size) {+            len = b->size - loc;+        }+        fwrite((b->data)+loc, sizeof(uint8_t), len, h);+    }+}+
+ rts/idris_buffer.h view
@@ -0,0 +1,23 @@+#ifndef __BUFFER_H+#define __BUFFER_H++#include <stdlib.h>+#include <stdio.h>+#include <stdint.h>++void* idris_newBuffer(int bytes);++int idris_getBufferSize(void* buffer);++void idris_setBufferByte(void* buffer, int loc, uint8_t byte);+void idris_setBufferString(void* buffer, int loc, char* str);++void idris_copyBuffer(void* from, int start, int len,+                      void* to, int loc);++int idris_readBuffer(FILE* h, void* buffer, int loc, int max);+void idris_writeBuffer(FILE* h, void* buffer, int loc, int len);++uint8_t idris_getBufferByte(void* buffer, int loc);++#endif
rts/idris_rts.c view
@@ -239,6 +239,11 @@ #endif         return ptr;     } else {+        // If we're trying to allocate something bigger than the heap,+        // grow the heap here so that the new heap is big enough.+        if (size > vm->heap.size) {+            vm->heap.size += size;+        }         idris_gc(vm); #ifdef HAS_PTHREAD         if (lock) { // not message passing@@ -595,6 +600,22 @@     return ret; } +VAL idris_readChars(VM* vm, int num, FILE* h) {+    VAL ret;+    char *buffer = malloc((num+1)*sizeof(char));+    size_t len;+    len = fread(buffer, sizeof(char), (size_t)num, h);+    buffer[len] = '\0';++    if (len <= 0) {+        ret = MKSTR(vm, "");+    } else {+        ret = MKSTR(vm, buffer);+    }+    free(buffer);+    return ret;+}+ void idris_crash(char* msg) {     fprintf(stderr, "%s\n", msg);     exit(1);@@ -615,7 +636,7 @@     return cl; } -VAL idris_strTail(VM* vm, VAL str) {+VAL idris_strShift(VM* vm, VAL str, int num) {     // If there's no room, just copy the string, or we'll have a problem after     // gc moves str     if (space(vm, sizeof(Closure) + sizeof(StrOffset))) {@@ -633,7 +654,7 @@         }          cl->info.str_offset->str = root;-        cl->info.str_offset->offset = offset+idris_utf8_charlen(GETSTR(str));+        cl->info.str_offset->offset = offset+idris_utf8_findOffset(GETSTR(str), num);          return cl;     } else {@@ -642,6 +663,10 @@     } } +VAL idris_strTail(VM* vm, VAL str) {+    return idris_strShift(vm, str, 1);+}+ VAL idris_strCons(VM* vm, VAL x, VAL xs) {     char *xstr = GETSTR(xs);     int xval = GETINT(x);@@ -671,14 +696,24 @@ }  VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {-    char *start = idris_utf8_advance(GETSTR(str), GETINT(offset));-    char *end = idris_utf8_advance(start, GETINT(length));-    Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);-    SETTY(newstr, CT_STRING);-    newstr -> info.str = (char*)newstr + sizeof(Closure);-    memcpy(newstr -> info.str, start, end - start);-    *(newstr -> info.str + (end - start) + 1) = '\0';-    return newstr;+    int offset_val = GETINT(offset);+    int length_val = GETINT(length);+    char* str_val = GETSTR(str);++    // If the substring is a suffix, use idris_strShift to avoid reallocating+    if (offset_val + length_val >= strlen(str_val)) {+        return idris_strShift(vm, str, offset_val);+    }+    else {+        char *start = idris_utf8_advance(str_val, offset_val);+        char *end = idris_utf8_advance(start, length_val);+        Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);+        SETTY(newstr, CT_STRING);+        newstr -> info.str = (char*)newstr + sizeof(Closure);+        memcpy(newstr -> info.str, start, end - start);+        *(newstr -> info.str + (end - start) + 1) = '\0';+        return newstr;+    } }  VAL idris_strRev(VM* vm, VAL str) {
rts/idris_rts.h view
@@ -372,9 +372,13 @@ VAL idris_strlt(VM* vm, VAL l, VAL r); VAL idris_streq(VM* vm, VAL l, VAL r); VAL idris_strlen(VM* vm, VAL l);+// Read a line from a file VAL idris_readStr(VM* vm, FILE* h);+// Read up to 'num' characters from a file+VAL idris_readChars(VM* vm, int num, FILE* h);  VAL idris_strHead(VM* vm, VAL str);+VAL idris_strShift(VM* vm, VAL str, int num); VAL idris_strTail(VM* vm, VAL str); // This is not expected to be efficient! Mostly we wouldn't expect to call // it at all at run time.
rts/idris_stdfgn.c view
@@ -142,3 +142,36 @@ void idris_forceGC(void* vm) {     idris_gc((VM*)vm); }++typedef struct {+    char* string;+    int len;+} StrBuffer;++void* idris_makeStringBuffer(int len) {+    StrBuffer* sb = malloc(sizeof(StrBuffer));+    if (sb != NULL) {+        sb->string = malloc(len);+        sb->string[0] = '\0';+        sb->len = 0;+    }+    return sb;+}++void idris_addToString(void* buffer, char* str) {+    StrBuffer* sb = (StrBuffer*)buffer;+    int len = strlen(str);++    memcpy(sb->string + sb->len, str, len+1);+    sb->len += len;+}++VAL idris_getString(VM* vm, void* buffer) {+    StrBuffer* sb = (StrBuffer*)buffer;++    VAL str = MKSTR(vm, sb->string);+    free(sb->string);+    free(sb);+    return str;+}+
rts/idris_stdfgn.h view
@@ -20,6 +20,12 @@ // construct a file error structure (see Prelude.File) from errno VAL idris_mkFileError(VM* vm); +// Some machinery for building a large string without reallocating+// Create a string with space for 'len' bytes+void* idris_makeStringBuffer(int len);+void idris_addToString(void* buffer, char* str);+VAL idris_getString(VM* vm, void* buffer);+ void* do_popen(const char* cmd, const char* mode); int fpoll(void* h);
rts/idris_utf8.c view
@@ -103,6 +103,17 @@     return str; } +int idris_utf8_findOffset(char* str, int i) {+    int offset = 0;+    while(i > 0) {+        int len = idris_utf8_charlen(str);+        str+=len;+        offset+=len;+        i--;+    }+    return offset;+}+  char* idris_utf8_fromChar(int x) {     char* str;
rts/idris_utf8.h view
@@ -21,4 +21,6 @@ // Advance a pointer into a string by i UTF8 characters. // Return original pointer if i <= 0. char* idris_utf8_advance(char* str, int i);+// Return the offset of the ith UTF8 character in the string+int idris_utf8_findOffset(char* str, int i); #endif
+ samples/ST/Composite.idr view
@@ -0,0 +1,8 @@+import Control.ST++splitComp : (comp : Var) -> +            ST m () [comp ::: Composite [State Int, State String]]+splitComp comp = do [int, str] <- split comp+                    update int (+ 1)+                    update str (++ "\n")+                    combine comp [int, str]
+ samples/ST/Graphics/Draw.idr view
@@ -0,0 +1,88 @@+module Draw++import public Graphics.SDL+import Control.ST+import Control.ST.ImplicitCall++%access public export++data Col = MkCol Int Int Int Int++black : Col +black = MkCol 0 0 0 255++red : Col +red = MkCol 255 0 0 255++green : Col +green = MkCol 0 255 0 255++blue : Col +blue = MkCol 0 0 255 255++cyan : Col +cyan = MkCol 0 255 255 255++magenta : Col +magenta = MkCol 255 0 255 255++yellow : Col +yellow = MkCol 255 255 0 255++white : Col +white = MkCol 255 255 255 255++interface Draw (m : Type -> Type) where+  Surface : Type++  initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]+  closeWindow : (win : Var) -> ST m () [remove win Surface] ++  flip : (win : Var) -> ST m () [win ::: Surface]+  poll : ST m (Maybe Event) []++  filledRectangle : (win : Var) -> (Int, Int) -> (Int, Int) -> Col ->+                    ST m () [win ::: Surface]+  drawLine : (win : Var) -> (Int, Int) -> (Int, Int) -> Col ->+             ST m () [win ::: Surface]+++Draw IO where+  Surface = State SDLSurface++  initWindow x y = do Just srf <- lift (startSDL x y)+                           | pure Nothing+                      var <- new srf+                      pure (Just var)++  closeWindow win = do lift endSDL+                       delete win++  flip win = do srf <- read win+                lift (flipBuffers srf)+  poll = lift pollEvent++  filledRectangle win (x, y) (ex, ey) (MkCol r g b a)+       = do srf <- read win+            lift $ filledRect srf x y ex ey r g b a+  drawLine win (x, y) (ex, ey) (MkCol r g b a)+       = do srf <- read win+            lift $ drawLine srf x y ex ey r g b a++render : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]+render win = do filledRectangle win (0,0) (640,480) black+                drawLine win (100,100) (200,200) red+                flip win+    +loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]+loop win = do render win+              Just AppQuit <- poll+                   | _ => loop win+              pure ()++drawMain : (ConsoleIO m, Draw m) => ST m () []+drawMain = do Just win <- initWindow 640 480+                 | Nothing => putStrLn "Can't open window"+              loop win+              closeWindow win+
+ samples/ST/Graphics/Turtle.idr view
@@ -0,0 +1,116 @@+module Main++import Control.ST+import Control.ST.ImplicitCall+import Draw++interface TurtleGraphics (m : Type -> Type) where+  Turtle : Type++  start : Int -> Int -> ST m (Maybe Var) [addIfJust Turtle]+  end : (t : Var) -> ST m () [Remove t Turtle]++  fd : (t : Var) -> Int -> ST m () [t ::: Turtle]+  rt : (t : Var) -> Int -> ST m () [t ::: Turtle]++  penup : (t : Var) -> ST m () [t ::: Turtle]+  pendown : (t : Var) -> ST m () [t ::: Turtle]+  col : (t : Var) -> Col -> ST m () [t ::: Turtle]++  -- Render the picture drawn so far in a window, and wait for a key press+  render : (t : Var) -> ST m () [t ::: Turtle]++Line : Type+Line = ((Int, Int), (Int, Int), Col)++-- Implement turtle graphics in terms of existing stateful systems;+-- 'Draw' provides a Surface to draw on, and three states.+Draw m => TurtleGraphics m where+  Turtle = Composite [Surface {m}, -- surface to draw on+                      State Col,  -- pen colour+                      State (Int, Int, Int, Bool), -- pen location/direction/down+                      State (List Line)] -- lines to draw on render++  start x y = with ST do +                 Just srf <- initWindow x y+                      | Nothing => pure Nothing+                 col <- new white+                 pos <- new (320, 200, 0, True)+                 lines <- new []+                 turtle <- new ()+                 combine turtle [srf, col, pos, lines]+                 pure (Just turtle)++  end t = do [srf, col, pos, lines] <- split t+             closeWindow srf; delete col; delete pos; delete lines; delete t++  fd t dist = with ST do +                 [srf, col, pos, lines] <- split t+                 (x, y, d, p) <- read pos+                 let x' = cast x + cast dist * sin (rad d)+                 let y' = cast y + cast dist * cos (rad d)+                 c <- read col+                 ls <- read lines+                 write lines (if p then ((x, y), (cast x', cast y'), c) :: ls+                                   else ls)+                 write pos (cast x', cast y', d, p)+                 combine t [srf, col, pos, lines]+     where rad : Int -> Double+           rad x = (cast x * pi) / 180.0++  rt t angle = with ST do +                  [srf, col, pos, lines] <- split t+                  (x, y, d, p) <- read pos+                  write pos (x, y, d + angle `mod` 360, p)+                  combine t [srf, col, pos, lines]++  penup t = with ST do +               [srf, col, pos, lines] <- split t+               (x, y, d, _) <- read pos+               write pos (x, y, d, False)+               combine t [srf, col, pos, lines]+  pendown t = with ST do +                 [srf, col, pos, lines] <- split t+                 (x, y, d, _) <- read pos+                 write pos (x, y, d, True)+                 combine t [srf, col, pos, lines]+  col t c = with ST do +               [srf, col, pos, lines] <- split t+               write col c+               combine t [srf, col, pos, lines]++  render t = with ST do +                [srf, col, pos, lines] <- split t+                filledRectangle srf (0, 0) (640, 480) black+                drawAll srf !(read lines)+                flip srf+                combine t [srf, col, pos, lines]+                Just ev <- poll+                  | Nothing => render t+                case ev of+                     KeyUp _ => pure ()+                     _ => render t+   where drawAll : (srf : Var) -> List Line -> ST m () [srf ::: Surface {m}]+         drawAll srf [] = pure ()+         drawAll srf ((start, end, col) :: xs) +            = do drawLine srf start end col+                 drawAll srf xs++turtle : (ConsoleIO m, TurtleGraphics m) => ST m () []+turtle = with ST do +            Just t <- start 640 480+                 | Nothing => putStr "Can't make turtle\n"+            col t yellow+            fd t 100; rt t 90+            col t green+            fd t 100; rt t 90+            col t red+            fd t 100; rt t 90+            col t blue+            fd t 100; rt t 90+            render t+            end t++main : IO ()+main = run turtle+
+ samples/ST/Intro.idr view
@@ -0,0 +1,75 @@+import Control.ST+import Data.Vect++-- Basic state++-- increment : (x : Var) -> STrans m () [x ::: State Int] +--                                      (const [x ::: State Int])+increment : (x : Var) -> ST m () [x ::: State Int] +increment x = do num <- read x+                 write x (num + 1)++-- makeAndIncrement : Int -> STrans m Int [] (const [])+makeAndIncrement : Int -> ST m Int []+makeAndIncrement init = do var <- new init+                           increment var+                           x <- read var+                           delete var+                           pure x++ioMakeAndIncrementBad : STrans IO () [] (const [])+ioMakeAndIncrementBad +   = do lift $ putStr "Enter a number: "+        init <- lift $ getLine+        var <- new (cast init)+        lift $ putStrLn ("var = " ++ show !(read var))+        increment var+        lift $ putStrLn ("var = " ++ show !(read var))+        delete var++ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])+ioMakeAndIncrement +   = do putStr "Enter a number: "+        init <- getStr+        var <- new (cast init)+        putStrLn ("var = " ++ show !(read var))+        increment var+        putStrLn ("var = " ++ show !(read var))+        delete var++-- Dependent state++-- addElement : (vec : Var) -> (item : a) ->+--              STrans m () [vec ::: State (Vect n a)]+--                   (const [vec ::: State (Vect (S n) a)])+addElement : (vec : Var) -> (item : a) ->+             ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]+addElement vec item = do xs <- read vec+                         write vec (item :: xs)++addElement' : (vec : Var) -> (item : a) ->+              STrans m () [vec ::: State (Vect n a)]+                   (const [vec ::: State (Vect (S n) a)])+addElement' vec item = update vec (item ::)++-- readAndAdd : ConsoleIO io => (vec : Var) ->+--              STrans io Bool [vec ::: State (Vect n Integer)]+--                    (\res => [vec ::: State (if res then Vect (S n) Integer+--                                                    else Vect n Integer)])+readAndAdd : ConsoleIO io => (vec : Var) ->+             ST io Bool +                   [vec ::: State (Vect n Integer) :->+                            \res => State (if res then Vect (S n) Integer+                                                  else Vect n Integer)]+readAndAdd vec = do putStr "Enter a number: "+                    num <- getStr+                    if all isDigit (unpack num)+                       then returning True (update vec ((cast num) ::))+                       else returning False (pure ())++-- newState : STrans m Var [] (\lbl => [lbl ::: State Int])+newState : ST m Var [add (State Int)]++-- removeState : (lbl : Var) -> STrans m () [lbl ::: State Int] (const [])+removeState : (lbl : Var) -> ST m () [remove lbl (State Int)]+
+ samples/ST/Login.idr view
@@ -0,0 +1,55 @@+import Control.ST++data Access = LoggedOut | LoggedIn+data LoginResult = OK | BadPassword++interface DataStore (m : Type -> Type) where+  data Store : Access -> Type++  connect : ST m Var [add (Store LoggedOut)]+  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]+  +  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]+  login : (store : Var) ->+          ST m LoginResult [store ::: Store LoggedOut :->+                             (\res => Store (case res of+                                                  OK => LoggedIn+                                                  BadPassword => LoggedOut))]+  logout : (store : Var) ->+           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]++getData : (ConsoleIO m, DataStore m) => ST m () []+getData = do st <- connect+             OK <- login st+                | BadPassword => do putStrLn "Failure"+                                    disconnect st+             secret <- readSecret st+             putStrLn ("Secret is: " ++ show secret)+             logout st+             disconnect st++-- badGet : DataStore m => ST m () []+-- badGet = do st <- connect+--             secret <- readSecret st+--             disconnect st++DataStore IO where+  Store x = State String -- represents secret data++  connect = do store <- new "Secret Data"+               pure store++  disconnect store = delete store++  readSecret store = readSecret store++  login store = do putStr "Enter password: "+                   p <- getStr+                   if p == "Mornington Crescent"+                      then pure OK+                      else pure BadPassword+  logout store = pure ()++main : IO ()+main = run getData+
+ samples/ST/LoginCount.idr view
@@ -0,0 +1,77 @@+import Control.ST+import Control.ST.ImplicitCall++data Access = LoggedOut | LoggedIn+data LoginResult = OK | BadPassword++interface DataStore (m : Type -> Type) where+  data Store : Access -> Type++  connect : ST m Var [add (Store LoggedOut)]+  disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]+  +  readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]+  login : (store : Var) ->+          ST m LoginResult [store ::: Store LoggedOut :->+                             (\res => Store (case res of+                                                  OK => LoggedIn+                                                  BadPassword => LoggedOut))]+  logout : (store : Var) ->+           ST m () [store ::: Store LoggedIn :-> Store LoggedOut]++getData : (ConsoleIO m, DataStore m) => +          (failcount : Var) -> ST m () [failcount ::: State Integer]+getData failcount+   = do st <- call connect+        OK <- login st+           | BadPassword => do putStrLn "Failure"+                               fc <- read failcount+                               write failcount (fc + 1)+                               putStrLn ("Number of failures: " ++ show (fc + 1))+                               disconnect st+                               getData failcount+        secret <- readSecret st+        putStrLn ("Secret is: " ++ show secret)+        logout st+        disconnect st+        getData failcount++getData2 : (ConsoleIO m, DataStore m) => +           (st, failcount : Var) -> +           ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]+getData2 st failcount+   = do OK <- login st+           | BadPassword => do putStrLn "Failure"+                               fc <- read failcount+                               write failcount (fc + 1)+                               putStrLn ("Number of failures: " ++ show (fc + 1))+                               getData2 st failcount+        secret <- readSecret st+        putStrLn ("Secret is: " ++ show secret)+        logout st+        getData2 st failcount++DataStore IO where+  Store x = State String -- represents secret data++  connect = do store <- new "Secret Data"+               pure store++  disconnect store = delete store++  readSecret store = read store++  login store = do putStr "Enter password: "+                   p <- getStr+                   if p == "Mornington Crescent"+                      then pure OK+                      else pure BadPassword+  logout store = pure ()++main : IO ()+main = run (do fc <- new 0+               st <- connect+               getData2 st fc+               disconnect st+               delete fc)+
+ samples/ST/Net/EchoSimple.idr view
@@ -0,0 +1,24 @@+import Network.Socket+import Network+import Control.ST+import Control.ST.ImplicitCall++echoServer : (ConsoleIO m, Sockets m) => (sock : Var) -> +             ST m () [remove sock (Sock {m} Listening)]+echoServer sock = +  do Right new <- accept sock | Left err => do close sock; remove sock+     Right msg <- recv new | Left err => do close sock; remove sock; remove new+     Right ok <- send new ("You said " ++ msg)+           | Left err => do remove new; close sock; remove sock+     close new; remove new; echoServer sock++startServer : (ConsoleIO m, Sockets m) => ST m () [] +startServer = +  do Right sock <- socket Stream        | Left err => pure () +     Right ok <- bind sock Nothing 9442 | Left err => remove sock+     Right ok <- listen sock            | Left err => remove sock+     echoServer sock++main : IO ()+main = run startServer+
+ samples/ST/Net/Network.idr view
@@ -0,0 +1,106 @@+module Network++import Control.ST+import Network.Socket++public export+data SocketState = Ready+                 | Bound +                 | Listening+                 | Open +                 | Closed++public export+data CloseOK : SocketState -> Type where+     CloseOpen : CloseOK Open+     CloseListening : CloseOK Listening++-- Sockets API. By convention, the methods return 'Left' on failure or+-- 'Right' on success (even if the error/result is merely unit).+public export+interface Sockets (m : Type -> Type) where+  Sock : SocketState -> Type++  -- Create a new socket. If successful, it's in the Closed state+  socket : SocketType ->+           ST m (Either () Var) [addIfRight (Sock Ready)]++  -- Bind a socket to a port. If successful, it's moved to the Bound state.+  bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->+         ST m (Either () ()) +              [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]+  -- Listen for connections on a socket. If successful, it's moved to the+  -- Listening state+  listen : (sock : Var) ->+           ST m (Either () ())+              [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]+  -- Accept an incoming connection on a Listening socket. If successful, +  -- creates a new socket in the Open Server state, and keeps the existing+  -- socket in the Listening state+  accept : (sock : Var) ->+           ST m (Either () Var)+                [sock ::: Sock Listening, addIfRight (Sock Open)]++  -- Connect to a remote address on a socket. If successful, moves to the+  -- Open Client state+  connect : (sock : Var) -> SocketAddress -> Port ->+            ST m (Either () ())+               [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]+  +  -- Close an Open or Listening socket+  close : (sock : Var) ->+          {auto prf : CloseOK st} ->+          ST m () [sock ::: Sock st :-> Sock Closed]++  remove : (sock : Var) ->+           ST m () [Remove sock (Sock Closed)]++  -- Send a message on a connected socket.+  -- On failure, move the socket to the Closed state+  send : (sock : Var) -> String -> +         ST m (Either () ())+              [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]+  -- Receive a message on a connected socket+  -- On failure, move the socket to the Closed state+  recv : (sock : Var) ->+         ST m (Either () String)+              [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]++export+implementation Sockets IO where+  Sock _ = State Socket++  socket ty = do Right sock <- lift $ Socket.socket AF_INET ty 0+                      | Left err => pure (Left ())+                 lbl <- new sock+                 pure (Right lbl)+                +  bind sock addr port = do ok <- lift $ bind !(read sock) addr port+                           if ok /= 0+                              then pure (Left ())+                              else pure (Right ())+  listen sock = do ok <- lift $ listen !(read sock)+                   if ok /= 0+                      then pure (Left ())+                      else pure (Right ())+  accept sock = do Right (conn, addr) <- lift $ accept !(read sock)+                         | Left err => pure (Left ())+                   lbl <- new conn+                   returning (Right lbl) (toEnd lbl)++  connect sock addr port +       = do ok <- lift $ connect !(read sock) addr port+            if ok /= 0+               then pure (Left ())+               else pure (Right ())+  close sock = do lift $ close !(read sock)+                  pure ()+  remove sock = delete sock++  send sock msg = do Right _ <- lift $ send !(read sock) msg+                           | Left _ => pure (Left ())+                     pure (Right ())+  recv sock = do Right (msg, len) <- lift $ recv !(read sock) 1024 -- Yes, yes...+                       | Left _ => pure (Left ())+                 pure (Right msg)+
+ samples/ST/Net/RandServer.idr view
@@ -0,0 +1,156 @@+import Network.Socket+import Control.ST+import Control.ST.ImplicitCall+import System++import Network+import Threads++{- A random number server.++This receives requests from a client, as a number, and sends a reply+which is a random number within the requested bound.++There are two states: one for the server, and one for a connected session.+The server repeatedly listens for requests and creats a session for each+incoming request.+-}++-- States of a connected session+data SessionState = Waiting -- waiting for the client to send+                  | Processing -- calculating a response to send back+                  | Done -- received message and replied to it++interface RandomSession (m : Type -> Type) where+  -- A connected session+  Connection : SessionState -> Type+  -- A server listening for connections+  Server : Type++  -- Receive a request on a Waiting connection. If there is a request+  -- available, move to the Processing state+  recvReq : (conn : Var) ->+            ST m (Maybe Integer) +                 [conn ::: Connection Waiting :->+                           \res => Connection (case res of+                                                    Nothing => Done+                                                    Just _ => Processing)]+  -- Send a reply, and move the connection to the Done state+  sendResp : (conn : Var) -> Integer ->+             ST m () [conn ::: Connection Processing :-> Connection Done]++  -- Create a server+  start : ST m (Maybe Var) [addIfJust Server]+  -- Close a server+  quit : (srv : Var) -> ST m () [Remove srv Server]+  -- Finish a connection+  done : (conn : Var) -> ST m () [Remove conn (Connection Done)]++  -- Listen for an incoming connection. If there is one, create a session+  -- with a connection in the Waiting state+  accept : (srv : Var) ->+           ST m (Maybe Var) +                [srv ::: Server, addIfJust (Connection Waiting)]++interface Sleep (m : Type -> Type) where+  usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> +           STrans m () xs (const xs)++Sleep IO where+  usleep x = lift (System.usleep x)+++using (Sleep io, ConsoleIO io, RandomSession io, Conc io)+  rndSession : (conn : Var) -> +               ST io () [Remove conn (Connection {m=io} Waiting)]+  rndSession conn =+         do Just bound <- call (recvReq conn)+              | Nothing => do putStr "Nothing received\n"+                              call (done conn)+            putStr "Calculating reply...\n"+            usleep 1000000+            sendResp conn bound -- (seed `mod` (bound + 1))+            call (done conn)++  rndLoop : (srv : Var) -> ST io () [srv ::: Server {m=io}]+  rndLoop srv +    = do Just conn <- accept srv+              | Nothing => putStr "accept failed\n"+         putStr "Connection received\n"+         fork (rndSession conn)+         rndLoop srv++  rndServer : ST io () []+  rndServer +    = do Just srv <- start+              | Nothing => putStr "Can't start server\n"+         call (rndLoop srv)+         quit srv++implementation (ConsoleIO io, Sockets io) => RandomSession io where+  +  -- Connections and servers are composite states, so to implement things+  -- in terms of them we need to 'split' at the state and 'combine' at the+  -- end, in every method+  Connection Waiting = Composite [State Integer, Sock {m=io} Open]+  Connection Processing = Composite [State Integer, Sock {m=io} Open]+  Connection Done = Composite [State Integer, Sock {m=io} Closed]++  Server = Composite [State Integer, Sock {m=io} Listening]++  recvReq rec = do [seed, conn] <- split rec+                   Right msg <- recv conn+                         | Left err => do combine rec [seed, conn]+                                          pure Nothing+                   putStr ("Incoming " ++ show msg ++ "\n")+                   combine rec [seed, conn]+                   pure (Just (cast msg))++  sendResp rec val = do [seed, conn] <- split rec+                        Right () <- send conn (cast (!(read seed) `mod` val) ++ "\n")+                              | Left err => do combine rec [seed, conn]+                                               pure ()+                        close conn+                        combine rec [seed, conn]+  +  start = do srv <- new ()+             Right sock <- socket Stream+                   | Left err => do delete srv; pure Nothing+             Right () <- bind sock Nothing 9442+                   | Left err => do call (remove sock)+                                    delete srv+                                    pure Nothing+             Right () <- listen sock+                   | Left err => do call (remove sock)+                                    delete srv+                                    pure Nothing+             putStr "Started server\n"+             seed <- new 12345+             combine srv [seed, sock]+             pure (Just srv)+  +  quit srv = do [seed, sock] <- split srv -- need to delete everything+                close sock; remove sock; delete seed; delete srv+  done conn = do [seed, sock] <- split conn -- need to delete connection data+                 remove sock; delete seed; delete conn+  +  accept srv = do [seed, sock] <- split srv+                  seedVal <- read seed+                  write seed ((1664525 * seedVal + 1013904223) +                                `prim__sremBigInt` (pow 2 32))+                  Right conn <- accept sock+                        | Left err => do combine srv [seed, sock]+                                         pure Nothing -- no incoming message+                  -- We're sending the seed to the child process and keeping+                  -- a copy ourselves, so we need to explicitly make a new+                  -- one+                  rec <- new ()+                  seed' <- new seedVal+                  combine rec [seed', conn]+                  combine srv [seed, sock]+                  toEnd rec+                  pure (Just rec)++main : IO ()+main = run rndServer+
+ samples/ST/Net/Threads.idr view
@@ -0,0 +1,23 @@+module Threads++import Control.ST+import System.Concurrency.Channels+import System++public export+interface Conc (m : Type -> Type) where+  -- 'Fork' sends some resources to the spawned thread, and keeps the rest+  -- for the parent+  -- TODO: Note that there is nothing here yet about how the threads+  -- communicate with each other...+  fork : (thread : STrans m () thread_res (const [])) ->+         {auto tprf : SubRes thread_res all} ->+         STrans m () all (const (kept tprf)) ++export+implementation Conc IO where+  fork thread+      = do threadEnv <- dropSub+           lift $ spawn (do runWith threadEnv thread+                            pure ()) +           pure ()
+ samples/ST/TreeTag.idr view
@@ -0,0 +1,29 @@+import Control.ST++data BTree a = Leaf+             | Node (BTree a) a (BTree a)++testTree : BTree String+testTree = Node (Node Leaf "Jim" Leaf)+                "Fred"+                (Node (Node Leaf "Alice" Leaf)+                      "Sheila"+                      (Node Leaf "Bob" Leaf))+++treeTagAux : (tag : Var) -> BTree a -> ST m (BTree (Int, a)) [tag ::: State Int]+treeTagAux tag Leaf = pure Leaf+treeTagAux tag (Node left val right) +    = do left' <- treeTagAux tag left+         thisTag <- read tag+         write tag (thisTag + 1)+         right' <- treeTagAux tag right+         pure (Node left' (thisTag, val) right')++treeTag : (i : Int) -> BTree a -> BTree (Int, a)+treeTag i tree = runPure (do tag <- new i+                             t <- treeTagAux tag tree+                             delete tag+                             pure t)+            +
samples/misc/interp.idr view
@@ -1,5 +1,9 @@ module Main +import Data.Vect++%language DSLNotation+ data Ty = TyInt | TyBool | TyFun Ty Ty  interpTy : Ty -> Type@@ -14,30 +18,33 @@       (::) : interpTy a -> Env G -> Env (a :: G)    data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where-      stop : HasType FZ (t :: G) t-      pop  : HasType k G t -> HasType (FS k) (u :: G) t+      Stop : HasType FZ (t :: G) t+      Pop  : HasType k G t -> HasType (FS k) (u :: G) t    lookup : HasType i G t -> Env G -> interpTy t-  lookup stop    (x :: xs) = x-  lookup (pop k) (x :: xs) = lookup k xs+  lookup Stop    (x :: xs) = x+  lookup (Pop k) (x :: xs) = lookup k xs    data Expr : Vect n Ty -> Ty -> Type where       Var : HasType i G t -> Expr G t       Val : (x : Int) -> Expr G TyInt       Lam : Expr (a :: G) t -> Expr G (TyFun a t)-      App : Expr G (TyFun a t) -> Expr G a -> Expr G t+      App : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t       Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->             Expr G c       If  : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a       Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b +  lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)+  lam_ _ = Lam+   dsl expr-      lambda      = Lam+      lambda      = lam_       variable    = Var-      index_first = stop-      index_next  = pop+      index_first = Stop+      index_next  = Pop -  (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t+  (<*>) : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t   (<*>) = \f, a => App f a    pure : Expr G a -> Expr G a@@ -53,14 +60,16 @@    implementation Num (Expr G TyInt) where     (+) x y = Op (+) x y-    (-) x y = Op (-) x y     (*) x y = Op (*) x y -    abs x = IF (x < 0) THEN (-x) ELSE x-     fromInteger = Val . fromInteger+  +  implementation Neg (Expr G TyInt) where+    (-) x y = Op (-) x y+    abs x = IF (x < 0) THEN (-x) ELSE x+    negate x = Op (-) 0 x -  interp : Env G -> {static} Expr G t -> interpTy t+  interp : Env G -> Expr G t -> interpTy t   interp env (Var i)     = lookup i env   interp env (Val x)     = x   interp env (Lam sc)    = \x => interp (x :: env) sc@@ -79,7 +88,7 @@   eAdd = expr (\x, y => Op (+) x y)    eDouble : Expr G (TyFun TyInt TyInt)-  eDouble = expr (\x => App (App eAdd x) (Var stop))+  eDouble = expr (\x => App (App eAdd x) (Var Stop))    eFac : Expr G (TyFun TyInt TyInt)   eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)
src/IRTS/CodegenC.hs view
@@ -624,6 +624,10 @@ doOp v (LExternal rf) [_,x]    | rf == sUN "prim__readFile"        = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"+doOp v (LExternal rf) [_,len,x]+   | rf == sUN "prim__readChars"+       = v ++ "idris_readChars(vm, GETINT(" ++ creg len +++                                "), GETPTR(" ++ creg x ++ "))" doOp v (LExternal wf) [_,x,s]    | wf == sUN "prim__writeFile"        = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x
src/IRTS/CodegenJavaScript.hs view
@@ -757,19 +757,19 @@             )           ] -      | (LTrunc (ITFixed IT16) (ITFixed IT8)) <- op+      | (LTrunc (ITFixed _from) (ITFixed IT8)) <- op       , (arg:_)                               <- args =           jsPackUBits8 (             JSBinOp "&" (jsUnPackBits $ translateReg arg) (JSNum (JSInt 0xFF))           ) -      | (LTrunc (ITFixed IT32) (ITFixed IT16)) <- op+      | (LTrunc (ITFixed _from) (ITFixed IT16)) <- op       , (arg:_)                                <- args =           jsPackUBits16 (             JSBinOp "&" (jsUnPackBits $ translateReg arg) (JSNum (JSInt 0xFFFF))           ) -      | (LTrunc (ITFixed IT64) (ITFixed IT32)) <- op+      | (LTrunc (ITFixed _from) (ITFixed IT32)) <- op       , (arg:_)                                <- args =           jsPackUBits32 (             jsMeth (jsMeth (translateReg arg) "and" [
src/Idris/AbsSyntax.hs view
@@ -2204,7 +2204,7 @@     su (PAlternative ms b alts)        = let alts' = filter (/= Placeholder) (map su alts) in              if null alts' then Placeholder-                           else PAlternative ms b alts'+                           else liftHidden $ PAlternative ms b alts'     su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)     su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)     su t@(PLam fc _ _ _ _) = PHidden t@@ -2213,6 +2213,20 @@     su t = t      ctxt = tt_ctxt i++    -- If the ambiguous terms are all hidden, the PHidden needs to be outside+    -- because elaboration of PHidden gets delayed, and we need the elaboration+    -- to resolve the ambiguity.+    liftHidden tm@(PAlternative ms b as)+        | allHidden as = PHidden (PAlternative ms b (map unHide as))+        | otherwise = tm++    allHidden [] = True+    allHidden (PHidden _ : xs) = allHidden xs+    allHidden (x : xs) = False++    unHide (PHidden t) = t+    unHide t = t  stripUnmatchable i tm = tm
src/Idris/AbsSyntaxTree.hs view
@@ -1871,11 +1871,16 @@           depth d . bracket p startPrec $           lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>           st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc+      | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc       | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc       where         showRig Rig0 n = text "0" <+> prettyBindingOf n True         showRig Rig1 n = text "1" <+> prettyBindingOf n True         showRig _ n = prettyBindingOf n True++        isPi (PPi (Exp{}) _ _ _ _) = True+        isPi (PPi _ _ _ _ sc) = isPi sc+        isPi _ = False          st =           case s of
src/Idris/Core/Elaborate.hs view
@@ -611,9 +611,7 @@     mkClaims _ _ _ _             | Var n <- fn                    = do ctxt <- get_context-                        case lookupTy n ctxt of-                                [] -> lift $ tfail $ NoSuchVariable n-                                _ -> lift $ tfail $ TooManyArguments n+                        lift $ tfail $ TooManyArguments n             | otherwise = fail $ "Too many arguments for " ++ show fn      doClaim ((i, _), n, t) = do claim n t@@ -965,12 +963,14 @@        = do s <- get             ps <- get_probs             ivs <- get_implementations+            g <- goal             case prunStateT pmax True ps (if constrok then Nothing                                                       else Just ivs) x s of                 OK ((v, newps, probs), s') ->                       do let cs' = if (newps < pmax)                                       then [do put s'; return $! v]                                       else (do put s'; return $! v) : cs+                         put s                          doAll cs' newps xs                 Error err -> do put s                                 doAll cs pmax xs
src/Idris/Core/Execute.hs view
@@ -29,6 +29,7 @@ import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE) import Control.Monad.Trans.State.Strict import Data.Bits+import Data.IORef import qualified Data.Map as M import Data.Maybe import Data.Time.Clock.POSIX (getPOSIXTime)@@ -70,7 +71,12 @@              | forall a. EPtr (Ptr a)              | EThunk Context ExecEnv Term              | EHandle Handle+             | EStringBuf (IORef String) +mkRaw :: ExecVal -> ExecVal+mkRaw arg = EApp (EApp (EP (DCon 0 1 False) (sNS (sUN "MkRaw") ["FFI_C"]) EErased)+                       EErased) arg+ instance Show ExecVal where   show (EP _ n _)        = show n   show (EV i)            = "!!V" ++ show i ++ "!!"@@ -83,6 +89,7 @@   show (EPtr p)          = "<<ptr " ++ show p ++ ">>"   show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"   show (EHandle h)       = "<<handle " ++ show h ++ ">>"+  show (EStringBuf h)    = "<<string buffer>>"  toTT :: ExecVal -> Exec Term toTT (EP nt n ty) = (P nt n) <$> (toTT ty)@@ -117,6 +124,7 @@                              return (n, RigW, Let Erased v') toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution." toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."+toTT (EStringBuf ptr) = execFail $ Msg "Can't convert string buffers back to TT after execution."  unApplyV :: ExecVal -> (ExecVal, [ExecVal]) unApplyV tm = ua [] tm@@ -191,7 +199,7 @@                         | otherwise      = execFail . Msg $ "env too small" doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v                                              doExec ((n, v'):env) ctxt body-doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined+doExec env ctxt (Bind n (NLet t v) body) = undefined doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)                                         return $                                           EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)@@ -404,7 +412,38 @@             execIO $ hSetBuffering stdout NoBuffering             execApp env ctxt ioUnit (drop arity xs) +    -- Just use a Haskell String in an IORef for a string buffer+    | Just (FFun "idris_makeStringBuffer" [(_, len)] _) <- foreignFromTT arity ty fn xs+       = case len of+              EConstant (I _) -> do buf <- execIO $ newIORef ""+                                    let res = ioWrap (EStringBuf buf)+                                    execApp env ctxt res (drop arity xs) +              _ -> execFail . Msg $+                      "The argument to idris_makeStringBuffer should be an Int, but it was " +++                      show len +++                      ". Are all cases covered?"+    | Just (FFun "idris_addToString" [(_, strBuf), (_, str)] _) <- foreignFromTT arity ty fn xs+       = case (strBuf, str) of+              (EStringBuf ref, EConstant (Str add)) ->+                  do execIO $ modifyIORef ref (++add)+                     execApp env ctxt ioUnit (drop arity xs)+              _ -> execFail . Msg $+                      "The arguments to idris_addToString should be a StringBuffer and a String, but were " +++                      show strBuf ++ " and " ++ show str +++                      ". Are all cases covered?"+    | Just (FFun "idris_getString" [_, (_, str)] _) <- foreignFromTT arity ty fn xs+       = case str of+              EStringBuf ref -> do str <- execIO $ readIORef ref+                                   let res = ioWrap (mkRaw (EConstant (Str str)))+                                   execApp env ctxt res (drop arity xs)+              _ -> execFail . Msg $+                      "The argument to idris_getString should be a StringBuffer, but it was " +++                      show str +++                      ". Are all cases covered?"+++ -- Right now, there's no way to send command-line arguments to the executor, -- so just return 0. execForeign env ctxt arity ty fn xs onfail@@ -438,6 +477,7 @@ deNS n = n  prf = sUN "prim__readFile"+prc = sUN "prim__readChars" pwf = sUN "prim__writeFile" prs = sUN "prim__readString" pws = sUN "prim__writeString"@@ -479,6 +519,16 @@     | fn == prf =               Just (do contents <- execIO $ hGetLine h                        return (EConstant (Str (contents ++ "\n"))), xs)+getOp fn (_ : EConstant (I len) : EHandle h : xs)+    | fn == prc =+              Just (do contents <- execIO $ hGetChars h len+                       return (EConstant (Str contents)), xs)+  where hGetChars h 0 = return ""+        hGetChars h i = do eof <- hIsEOF h+                           if eof then return "" else do+                             c <- hGetChar h+                             rest <- hGetChars h (i - 1)+                             return (c : rest) getOp fn (_ : arg : xs)     | fn == prf =               Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)
src/Idris/Core/Unify.hs view
@@ -303,11 +303,17 @@      injective (P (DCon _ _ _) _ _) = True     injective (P (TCon _ _) _ _) = True-    injective (P Ref n _)-         | Just i <- lookupInjectiveExact n ctxt = i+--     injective (P Ref n _)+--          | Just i <- lookupInjectiveExact n ctxt = i     injective (App _ f a)        = injective f -- && injective a     injective _                  = False +--     injectiveTC (P Ref n _) (P Ref n' _)+--          | Just i <- lookupInjectiveExact n ctxt,+--            n == n' = i+--     injectiveTC (App _ f a) (App _ f' a') = injectiveTC f a+--     injectiveTC _ _ = False+ --     injectiveVar (P _ (MN _ _) _) = True -- TMP HACK     injectiveVar (P _ n _)        = n `elem` inj     injectiveVar (App _ f a)      = injectiveVar f -- && injective a@@ -534,6 +540,7 @@          | (injectiveApp fx && injectiveApp fy)         || (injectiveApp fx && metavarApp fy && ax == ay)         || (injectiveApp fy && metavarApp fx && ax == ay)+        || (injectiveTC fx fy) -- data interface method          = do let (headx, _) = unApply fx               let (heady, _) = unApply fy               -- fail quickly if the heads are disjoint@@ -611,6 +618,15 @@                            _ -> False              notFn t = injective t || metavar t || inenv t++            injectiveTC t@(P Ref n _) t'@(P Ref n' _)+                | Just ni <- lookupInjectiveExact n ctxt,+                  Just ni' <- lookupInjectiveExact n' ctxt+              = (n == n' && ni) ||+                (ni && metavar t') ||+                (metavar t && ni')+            injectiveTC (App _ f a) (App _ f' a') = injectiveTC f f'+            injectiveTC _ _ = False       unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
src/Idris/Coverage.hs view
@@ -14,6 +14,7 @@ import Idris.Core.Evaluate import Idris.Core.TT import Idris.Delaborate+import Idris.Elab.Utils import Idris.Error import Idris.Output (iWarn, iputStrLn) @@ -28,33 +29,64 @@ -- -- We need this to eliminate the pattern clauses which have been -- provided explicitly from new clause generation.+--+-- This takes a type directed approach to disambiguating names. If we+-- can't immediately disambiguate by looking at the expected type, it's an+-- error (we can't do this the usual way of trying it to see what type checks+-- since the whole point of an impossible case is that it won't type check!) mkPatTm :: PTerm -> Idris Term mkPatTm t = do i <- getIState                let timp = addImpl' True [] [] [] i t-               evalStateT (toTT (mapPT deNS timp)) 0+               evalStateT (toTT Nothing timp) 0   where-    toTT (PRef _ _ n) = do i <- lift getIState-                           case lookupNameDef n (tt_ctxt i) of-                                [(n', TyDecl nt _)] -> return $ P nt n' Erased-                                _ -> return $ P Ref n Erased-    toTT (PApp _ t args) = do t' <- toTT t-                              args' <- mapM (toTT . getTm) args-                              return $ mkApp t' args'-    toTT (PDPair _ _ _ l _ r) = do l' <- toTT l-                                   r' <- toTT r-                                   return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']-    toTT (PPair _ _ _ l r) = do l' <- toTT l-                                r' <- toTT r-                                return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']+    toTT :: Maybe Type -> PTerm -> StateT Int Idris Term+    toTT ty (PRef _ _ n)+       = do i <- lift getIState+            case lookupDefExact n (tt_ctxt i) of+                 Just (TyDecl nt _) -> return $ P nt n Erased+                 _ -> return $ P Ref n Erased+    toTT ty (PApp _ t@(PRef _ _ n) args)+       = do i <- lift getIState+            let aTys = case lookupTyExact n (tt_ctxt i) of+                              Just nty -> map (Just . snd) (getArgTys nty)+                              Nothing -> map (const Nothing) args+            args' <- zipWithM toTT aTys (map getTm args)+            t' <- toTT Nothing t+            return $ mkApp t' args'+    toTT ty (PApp _ t args)+       = do t' <- toTT Nothing t+            args' <- mapM (toTT Nothing . getTm) args+            return $ mkApp t' args'+    toTT ty (PDPair _ _ _ l _ r)+       = do l' <- toTT Nothing l+            r' <- toTT Nothing r+            return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']+    toTT ty (PPair _ _ _ l r)+       = do l' <- toTT Nothing l+            r' <- toTT Nothing r+            return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']     -- For alternatives, pick the first and drop the namespaces. It doesn't     -- really matter which is taken since matching will ignore the namespace.-    toTT (PAlternative _ _ (a : as)) = toTT a-    toTT _ = do v <- get-                put (v + 1)-                return (P Bound (sMN v "imp") Erased)+    toTT (Just ty) (PAlternative _ _ as)+       | (hd, _) <- unApply ty+          = do i <- lift getIState+               case pruneByType True [] hd ty i as of+                    [a] -> toTT (Just ty) a+                    _ -> lift $ ierror $ CantResolveAlts (map getAltName as)+    toTT Nothing (PAlternative _ _ as)+                    = lift $ ierror $ CantResolveAlts (map getAltName as)+    toTT ty _+       = do v <- get+            put (v + 1)+            return (P Bound (sMN v "imp") Erased) -    deNS (PRef f hl (NS n _)) = PRef f hl n-    deNS t = t+    getAltName (PApp _ (PRef _ _ (UN l)) [_, _, arg])+             | l == txt "Delay" = getAltName (getTm arg)+    getAltName (PApp _ (PRef _ _ n) _) = n+    getAltName (PRef _ _ n) = n+    getAltName (PApp _ h _) = getAltName h+    getAltName (PHidden h) = getAltName h+    getAltName x = sUN "_" -- should never happen here  -- | Given a list of LHSs, generate a extra clauses which cover the remaining -- cases. The ones which haven't been provided are marked 'absurd' so@@ -74,7 +106,9 @@         let lhs_given = zipWith removePlaceholders lhs_tms                             (map (stripUnmatchable i) (map flattenArgs given)) -        logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))+        logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map showTmImpls given)+        logCoverage 10 $ "Building coverage tree for:\n" ++ showSep "\n" (map show lhs_given)+        logCoverage 10 $ "From terms:\n" ++ showSep "\n" (map show lhs_tms)         let givenpos = mergePos (map getGivenPos given)          (cns, ctree_in) <-@@ -337,7 +371,14 @@                    ((P _ x _, _), (P _ y _, _)) -> x == y                    _ -> False validCoverageCase ctxt (InfiniteUnify _ _ _) = False-validCoverageCase ctxt (CantConvert _ _ _) = False+validCoverageCase ctxt (CantConvert topx topy _)+    = let topx' = normalise ctxt [] topx+          topy' = normalise ctxt [] topy in+          not (sameFam topx' topy')+  where sameFam topx topy+            = case (unApply topx, unApply topy) of+                   ((P _ x _, _), (P _ y _, _)) -> x == y+                   _ -> False validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e@@ -350,62 +391,82 @@     = let topx' = normalise ctxt [] topx           topy' = normalise ctxt [] topy in           evalState (checkRec topx' topy') []-  where -- different notion of recoverable than in unification, since we-        -- have no metavars -- just looking to see if a constructor is failing-        -- to unify with a function that may be reduced later, or if any-        -- variables need to have two different constructor forms--        -- The state is a mapping of name to what it has failed to unify-        -- with-        checkRec :: Term -> Term -> State [(Name, Term)] Bool-        checkRec (P Bound x _) tm-           | (P yt _ _, _) <- unApply tm,-             conType yt = do nmap <- get-                             case lookup x nmap of-                                  Nothing -> do put ((x, tm) : nmap)-                                                return True-                                  Just y' -> checkRec tm y'-        checkRec tm (P Bound y _)-           | (P xt _ _, _) <- unApply tm,-             conType xt = do nmap <- get-                             case lookup y nmap of-                                  Nothing -> do put ((y, tm) : nmap)-                                                return True-                                  Just x' -> checkRec tm x'-        checkRec (App _ f a) p@(P _ _ _) = checkRec f p-        checkRec p@(P _ _ _) (App _ f a) = checkRec p f-        checkRec fa@(App _ _ _) fa'@(App _ _ _)-            | (f, as) <- unApply fa,-              (f', as') <- unApply fa'-                 = if (length as /= length as')-                      then checkRec f f'-                      else checkRecs (f : as) (f' : as')-          where-            checkRecs [] [] = return True-            checkRecs (a : as) (b : bs) = do aok <- checkRec a b-                                             asok <- checkRecs as bs-                                             return (aok && asok)-        checkRec (P xt x _) (P yt y _)-           | x == y = return True-           | ntRec xt yt = return True-        checkRec _ _ = return False--        conType (DCon _ _ _) = True-        conType (TCon _ _) = True-        conType _ = False--        -- If either name is a reference or a bound variable, then further-        -- development may fix the error, so consider it recoverable.-        -- If both names are constructors, and the name is different, then-        -- it's not recoverable-        ntRec x y | Ref <- x = True-                  | Ref <- y = True-                  | Bound <- x = True-                  | Bound <- y = True-                  | otherwise = False -- name is different, unrecoverable+recoverableCoverage ctxt (CantConvert topx topy _)+    = let topx' = normalise ctxt [] topx+          topy' = normalise ctxt [] topy in+          evalState (checkRec topx' topy') [] recoverableCoverage ctxt (InfiniteUnify _ _ _) = False -- always unrecoverable recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e recoverableCoverage _ _ = False +-- different notion of recoverable than in unification, since we+-- have no metavars -- just looking to see if a constructor is failing+-- to unify with a function that may be reduced later, or if any+-- variables need to have two different constructor forms++-- The state is a mapping of name to what it has failed to unify+-- with+checkRec :: Term -> Term -> State [(Name, Term)] Bool+checkRec (P Bound x _) tm+   | (P yt _ _, _) <- unApply tm,+     conType yt = do nmap <- get+                     case lookup x nmap of+                          Nothing -> do put ((x, tm) : nmap)+                                        return True+                          Just y' -> checkRec tm y'+ where+   conType (DCon _ _ _) = True+   conType (TCon _ _) = True+   conType _ = False++checkRec tm (P Bound y _)+   | (P xt _ _, _) <- unApply tm,+     conType xt = do nmap <- get+                     case lookup y nmap of+                          Nothing -> do put ((y, tm) : nmap)+                                        return True+                          Just x' -> checkRec tm x'+ where+   conType (DCon _ _ _) = True+   conType (TCon _ _) = True+   conType _ = False++checkRec (App _ f a) p@(P _ _ _) = checkRec f p+checkRec p@(P _ _ _) (App _ f a) = checkRec p f+checkRec fa@(App _ _ _) fa'@(App _ _ _)+    | (f, as) <- unApply fa,+      (f', as') <- unApply fa'+         = if (length as /= length as')+              then checkRec f f'+              -- Same function but different args is recoverable,+              -- and vice versa, if it's an ordinary function+              -- If a constructor, everything has to be recoverable+              else do fok <- checkRec f f'+                      argok <- checkRecs (f : as) (f : as')+                      return (if conType f then fok && argok+                                           else fok || argok)+  where+    checkRecs [] [] = return True+    checkRecs (a : as) (b : bs) = do aok <- checkRec a b+                                     asok <- checkRecs as bs+                                     return (aok && asok)+    conType (P (DCon _ _ _) _ _) = True+    conType (P (TCon _ _) _ _) = True+    conType _ = False++checkRec (P xt x _) (P yt y _)+   | x == y = return True+   | ntRec xt yt = return True+ where+    -- If either name is a reference or a bound variable, then further+    -- development may fix the error, so consider it recoverable.+    -- If both names are constructors, and the name is different, then+    -- it's not recoverable+    ntRec x y | Ref <- x = True+              | Ref <- y = True+              | Bound <- x = True+              | Bound <- y = True+              | otherwise = False -- name is different, unrecoverable+checkRec _ _ = return False
src/Idris/DSL.hs view
@@ -53,23 +53,20 @@ expandSugar :: DSL -> PTerm -> PTerm expandSugar dsl (PLam fc n nfc ty tm)     | Just lam <- dsl_lambda dsl-        = let sc = PApp fc lam [ pexp (mkTTName fc n)-                               , pexp (var dsl n tm 0)]-          in expandSugar dsl sc+        = PApp fc lam [ pexp (mkTTName fc n)+                      , pexp (expandSugar dsl (var dsl n tm 0))] expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm) expandSugar dsl (PLet fc n nfc ty v tm)     | Just letb <- dsl_let dsl-        = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)-                                              , pexp v-                                              , pexp (var dsl n tm 0)]-          in expandSugar dsl sc+        = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)+                                     , pexp (expandSugar dsl v)+                                     , pexp (expandSugar dsl (var dsl n tm 0))] expandSugar dsl (PLet fc n nfc ty v tm) = PLet fc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm) expandSugar dsl (PPi p n fc ty tm)     | Just pi <- dsl_pi dsl-        = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)-                                            , pexp ty-                                            , pexp (var dsl n tm 0)]-          in expandSugar dsl sc+        = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)+                                   , pexp (expandSugar dsl ty)+                                   , pexp (expandSugar dsl (var dsl n tm 0))] expandSugar dsl (PPi p n fc ty tm) = PPi p n fc (expandSugar dsl ty) (expandSugar dsl tm) expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)                                         (map (fmap (expandSugar dsl)) args)
src/Idris/Delaborate.hs view
@@ -8,7 +8,7 @@ {-# LANGUAGE PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Delaborate (-    annName, bugaddr, delab, delabDirect, delab', delabMV, delabSugared+    annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared   , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab   , pprintDelabTy, pprintErr, resugar   ) where@@ -82,6 +82,9 @@ delab :: IState -> Term -> PTerm delab i tm = delab' i tm False False +delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm+delabWithEnv i tys tm = delabWithEnv' i tys tm False False+ delabMV :: IState -> Term -> PTerm delabMV i tm = delab' i tm False True @@ -89,26 +92,31 @@ -- 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+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 True-                         _ -> delabTy' i [] ty False False True+                         (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 True+delab' i t f mvs = delabTy' i [] [] t f mvs True +delabWithEnv' :: IState -> [(Name, Type)] -> Term -> Bool -> Bool -> PTerm+delabWithEnv' i tys t f mvs = delabTy' i [] tys t f mvs True+ delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any+          -> [(Name, Type)] -- ^ Names and types in environment+                            -- (for properly hiding scoped implicits)           -> Term           -> Bool -- ^ use full names           -> Bool -- ^ Don't treat metavariables specially           -> Bool -- ^ resugar cases           -> PTerm-delabTy' ist imps tm fullname mvs docases = de [] imps tm+delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm   where     un = fileFC "(val)" @@ -118,64 +126,71 @@     -- the last argument,     -- although that's not always the thing that gets pattern matched     -- in the elaborated block)-    de env imps sc+    de tys env imps sc           | docases           , isCaseApp sc           , (P _ cOp _, args@(_:_)) <- unApply sc-          , Just caseblock <- delabCase env imps (last args) cOp args+          , Just caseblock <- delabCase tys 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))+    de tys env _ (App _ f a) = deFn tys env f [a]+    de tys env _ (V i) | i < length env = PRef un [] (snd (env!!i))                        | otherwise = PRef un [] (sUN ("v" ++ show i ++ ""))-    de env _ (P _ n _) | n == unitTy = PTrue un IsType-                       | n == unitCon = PTrue un IsTerm-                       | Just n' <- lookup n env = PRef un [] n'-                       | otherwise-                            = case lookup n (idris_metavars ist) of-                                  Just (Just _, mi, _, _, _) -> mkMVApp n []-                                  _ -> PRef un [] n-    de env _ (Bind n (Lam _ ty) sc)-          = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)-    de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)+    de tys env _ (P _ n _) | n == unitTy = PTrue un IsType+                           | n == unitCon = PTrue un IsTerm+                           | Just n' <- lookup n env = PRef un [] n'+                           | otherwise+                                = case lookup n (idris_metavars ist) of+                                      Just (Just _, mi, _, _, _) -> mkMVApp n []+                                      _ -> PRef un [] n+    de tys env _ (Bind n (Lam _ ty) sc)+          = PLam un n NoFC (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) [] sc)+    de tys env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)        | toplevel_imp impl -- information in 'imps' repeated-          = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)-    de env is (Bind n (Pi rig (Just impl) ty _) sc)+          = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC+                (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)+    de tys env is (Bind n (Pi rig (Just impl) ty _) sc)        | tcimplementation impl-          = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)+          = PPi constraint n NoFC (de tys env [] ty)+                (de ((n, ty) : tys) ((n,n):env) is sc)        | otherwise-          = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)-    de env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)-          = PPi (Imp opts Dynamic False Nothing False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)-    de env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)-          = PPi (constraint { pcount = rig}) n NoFC (de env [] ty) (de ((n,n):env) is sc)-    de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)-          = PPi ((tacimpl tac) { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) is sc)-    de env (plic:is) (Bind n (Pi rig _ ty _) sc)+          = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de tys env [] ty) (de tys ((n,n):env) is sc)+    de tys env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)+          = PPi (Imp opts Dynamic False Nothing False rig) n NoFC+                (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)+    de tys env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)+          = PPi (constraint { pcount = rig}) n NoFC+                (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)+    de tys env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)+          = PPi ((tacimpl tac) { pcount = rig }) n NoFC+                (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)+    de tys env (plic:is) (Bind n (Pi rig _ ty _) sc)           = PPi (Exp (argopts plic) Dynamic False rig)                 n NoFC-                (de env [] ty)-                (de ((n,n):env) is sc)-    de env [] (Bind n (Pi rig _ ty _) sc)-          = PPi (expl { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) [] sc)+                (de tys env [] ty)+                (de ((n, ty) : tys) ((n,n):env) is sc)+    de tys env [] (Bind n (Pi rig _ ty _) sc)+          = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)+                (de ((n, ty) : tys) ((n,n):env) [] sc) -    de env imps (Bind n (Let ty val) sc)+    de tys env imps (Bind n (Let ty val) sc)           | docases           , isCaseApp sc           , (P _ cOp _, args) <- unApply sc-          , Just caseblock    <- delabCase env imps val cOp args = caseblock+          , Just caseblock    <- delabCase tys 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-    de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc-    de env plic (Bind n bb sc) = de ((n,n):env) [] sc-    de env _ (Constant i) = PConstant NoFC i-    de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"-    de env _ Erased = Placeholder-    de env _ Impossible = Placeholder-    de env _ (Inferred t) = Placeholder-    de env _ (TType i) = PType un-    de env _ (UType u) = PUniverse un u+              PLet un n NoFC (de tys env [] ty)+                   (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)+    de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc+    de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc+    de tys env plic (Bind n bb sc) = de ((n, binderTy bb) : tys) ((n,n):env) [] sc+    de tys env _ (Constant i) = PConstant NoFC i+    de tys env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"+    de tys env _ Erased = Placeholder+    de tys env _ Impossible = Placeholder+    de tys env _ (Inferred t) = Placeholder+    de tys env _ (TType i) = PType un+    de tys env _ (UType u) = PUniverse un u      dens x | fullname = x     dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of@@ -184,38 +199,48 @@                               _ -> ns     dens n = n -    deFn env (App _ f a) args = deFn env f (a:args)-    deFn env (P _ n _) [l,r]-         | n == pairTy    = PPair un [] IsType (de env [] l) (de env [] r)-         | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching-    deFn env (P _ n _) [ty, Bind x (Lam _ _) r]+    deFn tys env (App _ f a) args = deFn tys env f (a:args)+    deFn tys env (P _ n _) [l,r]+         | n == pairTy    = PPair un [] IsType (de tys env [] l) (de tys env [] r)+    deFn tys env (P _ n _) [ty, Bind x (Lam _ _) r]          | n == sigmaTy-               = PDPair un [] IsType (PRef un [] x) (de env [] ty)-                           (de ((x,x):env) [] (instantiate (P Bound x ty) r))-    deFn env (P _ n _) [lt,rt,l,r]-         | n == pairCon = PPair un [] IsTerm (de env [] l) (de env [] r)-         | n == sigmaCon = PDPair un [] IsTerm (de env [] l) Placeholder-                                                (de env [] r)-    deFn env f@(P _ n _) args-         | n `elem` map snd env-              = PApp un (de env [] f) (map pexp (map (de env []) args))-    deFn env (P _ n _) args+               = PDPair un [] IsType (PRef un [] x) (de tys env [] ty)+                           (de tys ((x,x):env) [] (instantiate (P Bound x ty) r))+    deFn tys env (P _ n _) [lt,rt,l,r]+         | n == pairCon = PPair un [] IsTerm (de tys env [] l) (de tys env [] r)+         | n == sigmaCon = PDPair un [] IsTerm (de tys env [] l) Placeholder+                                                (de tys env [] r)+--     deFn tys env f@(P _ n _) args+--          | n `elem` map snd env+--               = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))+    deFn tys env (P _ n _) args          | not mvs = case lookup n (idris_metavars ist) of                         Just (Just _, mi, _, _, _) ->-                            mkMVApp n (drop mi (map (de env []) args))-                        _ -> mkPApp n (map (de env []) args)-         | otherwise = mkPApp n (map (de env []) args)-    deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))+                            mkMVApp n (drop mi (map (de tys env []) args))+                        _ -> mkPApp tys n (map (de tys env []) args)+         | otherwise = mkPApp tys n (map (de tys env []) args)+    deFn tys env (V i) args+         | i < length env = mkPApp tys (fst (env!!i)) (map (de tys env []) args)+    deFn tys env f args = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))      mkMVApp n []             = PMetavar NoFC n     mkMVApp n args             = PApp un (PMetavar NoFC n) (map pexp args)-    mkPApp n args++    mkPApp tys n args+        | Just ty <- lookup n tys+            = let imps = findImp ty in+                  PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)         | Just imps <- lookupCtxtExact n (idris_implicits ist)             = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)         | otherwise = PApp un (PRef un [] n) (map pexp args)-+      where+        findImp (Bind n (Pi _ im@(Just i) _ _) sc)+             = pimp n Placeholder True : findImp sc+        findImp (Bind n (Pi _ _ _ _) sc)+             = pexp Placeholder : findImp sc+        findImp _ = []     imp (PImp p m l n _) arg = PImp p m l n arg     imp (PExp p l n _)   arg = PExp p l n arg     imp (PConstraint p l n _) arg = PConstraint p l n arg@@ -227,14 +252,14 @@             isCN (SN (CaseN _ _)) = True             isCN _ = False -    delabCase :: [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm-    delabCase env imps scrutinee caseName caseArgs =+    delabCase :: [(Name, Type)] -> [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm+    delabCase tys env imps scrutinee caseName caseArgs =       do cases <- case lookupCtxt caseName (idris_patdefs ist) of                     [(cases, _)] -> return cases                     _ -> Nothing-         return $ PCase un (de env imps scrutinee)-                    [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),-                       de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)+         return $ PCase un (de tys env imps scrutinee)+                    [ (de tys (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),+                       de tys (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)                     | (vars, lhs, rhs) <- cases                     ]       where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)@@ -268,8 +293,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 True-                         _ -> resugar i $ delabTy' i [] ty False False True+                         (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/Elab/Clause.hs view
@@ -611,6 +611,8 @@                                      return Nothing             -- if it's a recoverable error, the case may become possible             Error err -> do logLvl 10 $ "Impossible case " ++ (pshow i err)+                                 ++ "\n" ++ show (recoverableCoverage ctxt err,+                                                  validCoverageCase ctxt err)                             -- tcgen means that it was generated by genClauses,                             -- so only looking for an error. Otherwise, it                             -- needs to be the right kind of error (a type mismatch@@ -753,9 +755,6 @@          -- These are the names we're not allowed to use on the RHS, because         -- they're UniqueTypes and borrowed from another function.-        -- FIXME: There is surely a nicer way than this...-        -- Issue #1615 on the Issue Tracker.-        --     https://github.com/idris-lang/Idris-dev/issues/1615         when (not (null borrowed)) $           logElab 5 ("Borrowed names on LHS: " ++ show borrowed)
src/Idris/Elab/Data.hs view
@@ -193,9 +193,12 @@           -- Check that the constructor type is, in fact, a part of the family being defined          tyIs n cty'+         -- Need to calculate forceability from the non-normalised type,+         -- because we might not be able to export the definitions which+         -- we're normalising which changes the forceability status!          let force = if tn == sUN "Delayed"                         then [] -- TMP HACK! Totality checker needs this info-                        else forceArgs ctxt cty'+                        else forceArgs ctxt tn cty           logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t          logElab 5 $ "Inaccessible args: " ++ show inacc@@ -264,8 +267,8 @@         = tclift $ tfail (At fc (UniqueKindError AllTypes n))     checkUniqueKind _ _ = return () -forceArgs :: Context -> Type -> [Int]-forceArgs ctxt ty = forceFrom 0 ty+forceArgs :: Context -> Name -> Type -> [Int]+forceArgs ctxt tn ty = forceFrom 0 ty   where     -- for each argument, substitute in MN pos "FF"     -- then when we look at the return type, if we see MN pos name@@ -281,7 +284,8 @@         -- (FIXME: Actually the real risk is if we erase something a programmer         -- definitely wants, which is particularly the case with 'views'.         -- So perhaps we need a way of marking that in the source?)-        | (P _ ty _, args) <- unApply sc+        | (P _ ty _, args) <- unApply sc,+          ty == tn -- Must be the right top level type!              = if null (concatMap (findNonForcePos True) args)                   then nub (concatMap findForcePos args)                   else []
src/Idris/Elab/Interface.hs view
@@ -212,7 +212,7 @@                                           Just i -> i                                           Nothing -> []                          case lookupTyExact n (tt_ctxt ist) of-                              Just ty -> return (delabTy' ist impls ty False False False)+                              Just ty -> return (delabTy' ist impls [] ty False False False)                               Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))      -- Find the argument position of the current interface in a method type
src/Idris/Elab/Rewrite.hs view
@@ -76,9 +76,9 @@                         when (g == pred_tt) $ lift $ tfail (NoRewriting l r g)                         let pred = PLam fc rname fc Placeholder                                         (delab ist pred_tt)-                        let rewrite = stripImpls $-                                        addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)-                                              [pexp pred, pexp rule, pexp sc])+                        let rewrite = addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)+                                           [pexp (stripImpls pred),+                                            pexp (stripImpls rule), pexp sc]) --                         trace ("LHS: " ++ show l ++ "\n" ++ --                                "RHS: " ++ show r ++ "\n" ++ --                                "REWRITE: " ++ show rewrite ++ "\n" ++
src/Idris/Elab/Term.hs view
@@ -505,6 +505,7 @@               showHd (PApp _ (PRef _ _ n) _) = return n               showHd (PRef _ _ n) = return n               showHd (PApp _ h _) = showHd h+              showHd (PHidden h) = showHd h               showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here                doPrune as =@@ -615,7 +616,7 @@ --    elab' (_, _, inty) (PRef fc f) --       | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty --          = lift $ tfail (Msg "Typecase is not allowed")-    elab' ec _ tm@(PRef fc hl n)+    elab' ec fc' tm@(PRef fc hls n)       | pattern && not reflection && not (e_qq ec) && not (e_intype ec)             && isTConName n (tt_ctxt ist)               = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)@@ -628,22 +629,24 @@                  guarded = e_guarded ec                  inty = e_intype ec              ctxt <- get_context+             env <- get_env +             -- If the name is defined, globally or locally, elaborate it+             -- as a reference, otherwise it might end up as a pattern var.              let defined = case lookupTy n ctxt of-                               [] -> False+                               [] -> case lookupTyEnv n env of+                                          Just _ -> True+                                          _ -> False                                _ -> True-           -- this is to stop us resolve interfaces recursively-             -- trace (show (n, guarded)) $++             -- this is to stop us resolving interfaces recursively              if (tcname n && ina && not intransform)                then erun fc $                       do patvar n                          update_term liftPats                          highlightSource fc (AnnBoundName n False)-               else if defined-                       then do apply (Var n) []-                               annot <- findHighlight n-                               solve-                               highlightSource fc annot+               else if defined -- finally, ordinary PRef elaboration+                       then elabRef ec fc' fc hls n tm                        else try (do apply (Var n) []                                     annot <- findHighlight n                                     solve@@ -664,19 +667,7 @@               = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)           | pattern && not reflection && not (e_qq ina) && e_nomatching ina               = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)-          | otherwise =-               do fty <- get_type (Var n) -- check for implicits-                  ctxt <- get_context-                  env <- get_env-                  let a' = insertScopedImps fc (normalise ctxt env fty) []-                  if null a'-                     then erun fc $-                            do apply (Var n) []-                               hilite <- findHighlight n-                               solve-                               mapM_ (uncurry highlightSource) $-                                 (fc, hilite) : map (\f -> (f, hilite)) hls-                     else elab' ina fc' (PApp fc tm [])+          | otherwise = elabRef ina fc' fc hls n tm     elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"     elab' ina _ (PLam fc n nfc Placeholder sc)           = do -- if n is a type constructor name, this makes no sense...@@ -862,8 +853,10 @@             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+            knowns_m <- mapM getKnownImplicit args_in+            let knowns = mapMaybe id knowns_m+            args <- insertScopedImps fc f knowns (normalise ctxt env fty) args_in+             let unmatchableArgs = if pattern                                      then getUnmatchable (tt_ctxt ist) f                                      else []@@ -968,10 +961,10 @@                           es -> do put s                                    elab' ina topfc (PAppImpl tm es) -            checkKnownImplicit imp+            getKnownImplicit imp                  | UnknownImp `elem` argopts imp-                    = lift $ tfail $ UnknownImplicit (pname imp) f-            checkKnownImplicit _ = return ()+                    = return Nothing -- lift $ tfail $ UnknownImplicit (pname imp) f+                 | otherwise = return (Just (pname imp))              getReqImps (Bind x (Pi _ (Just i) ty _) sc)                  = i : getReqImps sc@@ -1302,27 +1295,36 @@              -- Delay dotted things to the end, then when we elaborate them              -- we can check the result against what was inferred              movelast h-             delayElab 10 $ do hs <- get_holes-                               when (h `elem` hs) $ do-                                   focus h-                                   dotterm-                                   elab' ina fc t+             (h' : hs) <- get_holes+             -- If we're at the end anyway, do it now+             if h == h' then elabHidden h+                        else delayElab 10 $ elabHidden h+     where+      elabHidden h = do hs <- get_holes+                        when (h `elem` hs) $ do+                            focus h+                            dotterm+                            elab' ina fc t     elab' ina fc (PRunElab fc' tm ns) =       do unless (ElabReflection `elem` idris_language_extensions ist) $            lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")          attack+         let elabName = sNS (sUN "Elab") ["Elab", "Reflection", "Language"]          n <- getNameFrom (sMN 0 "tacticScript")-         let scriptTy = RApp (Var (sNS (sUN "Elab")-                                  ["Elab", "Reflection", "Language"]))-                             (Var unitTy)+         let scriptTy = RApp (Var elabName) (Var unitTy)          claim n scriptTy          focus n+         elabUnit <- goal          attack -- to get an extra hole          elab' ina (Just fc') tm          script <- get_guess          fullyElaborated script          solve -- eliminate the hole. Because there are no references, the script is only in the binding+         ctxt <- get_context          env <- get_env+         (scriptTm, scriptTy) <- lift $ check ctxt [] (forget script)+         lift $ converts ctxt env elabUnit scriptTy+         env <- get_env          runElabAction info ist (maybe fc' id fc) env script ns          solve     elab' ina fc (PConstSugar constFC tm) =@@ -1508,15 +1510,41 @@     fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))     fullApp x = x -    insertScopedImps fc (Bind n (Pi _ im@(Just i) _ _) sc) xs-      | tcimplementation i && not (toplevel_imp i)-          = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs-      | not (toplevel_imp i)-          = pimp n Placeholder True : insertScopedImps fc sc xs-    insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)-        = x : insertScopedImps fc sc xs-    insertScopedImps _ _ xs = xs+    -- See if the name is listed as an implicit. If it is, return it, and+    -- drop it from the rest of the list+    findImplicit :: Name -> [PArg] -> (Maybe PArg, [PArg])+    findImplicit n [] = (Nothing, [])+    findImplicit n (i@(PImp _ _ _ n' _) : args)+        | n == n' = (Just i, args)+    findImplicit n (i@(PTacImplicit _ _ n' _ _) : args)+        | n == n' = (Just i, args)+    findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in+                                  (arg, x : rest) +    insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]+    insertScopedImps fc f knowns ty xs =+         do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs+            doInsert ty xs+      where+        doInsert ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs+          | (Just arg, xs') <- findImplicit n xs,+            not (toplevel_imp i)+              = liftM (arg :) (doInsert sc xs')+          | tcimplementation i && not (toplevel_imp i)+              = liftM (pimp n (PResolveTC fc) True :) (doInsert sc xs)+          | not (toplevel_imp i)+              = liftM (pimp n Placeholder True :) (doInsert sc xs)+        doInsert (Bind n (Pi _ _ _ _) sc) (x : xs)+              = liftM (x :) (doInsert sc xs)+        doInsert ty xs = return xs++        -- Any implicit in the application needs to have the name of a+        -- scoped implicit or a top level implicit, otherwise report an error+        checkKnownImplicit ns imp@(PImp{})+             | pname imp `elem` ns = return ()+             | otherwise = lift $ tfail $ At fc $ UnknownImplicit (pname imp) f+        checkKnownImplicit ns _ = return ()+     insertImpLam ina t =         do ty <- goal            env <- get_env@@ -1524,13 +1552,9 @@            addLam ty' t       where         -- just one level at a time-        addLam (Bind n (Pi _ (Just _) _ _) sc) t =+        addLam goal@(Bind n (Pi _ (Just _) _ _) sc) t =                  do impn <- unique_hole n -- (sMN 0 "scoped_imp")-                    if e_isfn ina -- apply to an implicit immediately-                       then return (PApp emptyFC-                                         (PLam emptyFC impn NoFC Placeholder t)-                                         [pexp Placeholder])-                       else return (PLam emptyFC impn NoFC Placeholder t)+                    return (PLam emptyFC impn NoFC Placeholder t)         addLam _ t = return t      insertCoerce ina t@(PCase _ _ _) = return t@@ -1555,6 +1579,21 @@                                 addImplBound ist (map fstEnv env)                                   (PApp fc (PRef fc [] n) [pexp (PCoerced t)]) +    elabRef :: ElabCtxt -> Maybe FC -> FC -> [FC] -> Name -> PTerm -> ElabD ()+    elabRef ina fc' fc hls n tm =+               do fty <- get_type (Var n) -- check for implicits+                  ctxt <- get_context+                  env <- get_env+                  a' <- insertScopedImps fc n [] (normalise ctxt env fty) []+                  if null a'+                     then erun fc $+                            do apply (Var n) []+                               hilite <- findHighlight n+                               solve+                               mapM_ (uncurry highlightSource) $+                                 (fc, hilite) : map (\f -> (f, hilite)) hls+                     else elab' ina fc' (PApp fc tm [])+     -- | Elaborate the arguments to a function     elabArgs :: IState -- ^ The current Idris state              -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)@@ -1659,167 +1698,6 @@     headIs f (PApp _ f' _) = headIs f f'     headIs f _ = True -- keep if it's not an application --- Rule out alternatives that don't return the same type as the head of the goal--- (If there are none left as a result, do nothing)-pruneByType :: Bool -> Env -> Term -> -- head of the goal-               Type -> -- goal-               IState -> [PTerm] -> [PTerm]--- if an alternative has a locally bound name at the head, take it-pruneByType imp env t goalty c as-   | Just a <- locallyBound as = [a]-  where-    locallyBound [] = Nothing-    locallyBound (t:ts)-       | Just n <- getName t,-         n `elem` map fstEnv env = Just t-       | otherwise = locallyBound ts-    getName (PRef _ _ n) = Just n-    getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays-       | l == txt "Delay" = getName (getTm arg)-    getName (PApp _ f _) = getName f-    getName (PHidden t) = getName t-    getName _ = Nothing---- 'n' is the name at the head of the goal type-pruneByType imp env (P _ n _) goalty ist as--- if the goal type is polymorphic, keep everything-   | Nothing <- lookupTyExact n ctxt = as--- if the goal type is a ?metavariable, keep everything-   | Just _ <- lookup n (idris_metavars ist) = as-   | otherwise-       = let asV = filter (headIs True n) as-             as' = filter (headIs False n) as in-             case as' of-               [] -> asV-               _ -> as'-  where-    ctxt = tt_ctxt ist--    -- Get the function at the head of the alternative and see if it's-    -- a plausible match against the goal type. Keep if so. Also keep if-    -- there is a possible coercion to the goal type.-    headIs var f (PRef _ _ f') = typeHead var f f'-    headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])-        | l == txt "Delay" = headIs var f (getTm arg)-    headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'-    headIs var f (PApp _ f' _) = headIs var f f'-    headIs var f (PPi _ _ _ _ sc) = headIs var f sc-    headIs var f (PHidden t) = headIs var f t-    headIs var f t = True -- keep if it's not an application--    typeHead var f f'-        = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $-          case lookupTyExact f' ctxt of-               Just ty -> case unApply (getRetTy ty) of-                            (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)-                                     -> False-                            _ -> let ty' = normalise ctxt [] ty in---                                    trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty---                                       ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $-                                     case unApply (getRetTy ty') of-                                          (V _, _) ->-                                              isPlausible ist var env n ty-                                          _ -> matchingTypes imp (getRetTy ty') goalty-                                                 || isCoercion (getRetTy ty') goalty--- May be useful to keep for debugging purposes for a bit:---                                                let res = matching (getRetTy ty') goalty in---                                                   traceWhen (not res)---                                                     ("Rejecting " ++ show (getRetTy ty', goalty)) res-               _ -> False--    matchingTypes True = matchingHead-    matchingTypes False = matching--    -- If the goal is a constructor, it must match the suggested function type-    matching (P _ ctyn _) (P _ n' _)-         | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'-         | otherwise = True-    -- Variables match anything-    matching (V _) _ = True-    matching _ (V _) = True-    matching _ (P _ n _) = not (isTConName n ctxt)-    matching (P _ n _) _ = not (isTConName n ctxt)-    -- Binders are a plausible match, so keep them-    matching (Bind n _ sc) _ = True-    matching _ (Bind n _ sc) = True-    -- If we hit a function name, it's a plausible match-    matching apl@(App _ _ _) apr@(App _ _ _)-         | (P _ fl _, argsl) <- unApply apl,-           (P _ fr _, argsr) <- unApply apr-       = fl == fr && and (zipWith matching argsl argsr)-           || (not (isConName fl ctxt && isConName fr ctxt))-    -- If the application structures aren't easily comparable, it's a-    -- plausible match-    matching (App _ f a) (App _ f' a') = True-    matching (TType _) (TType _) = True-    matching (UType _) (UType _) = True-    matching l r = l == r--    -- In impossible-case mode, only look at the heads (this is to account for-    -- the non type-directed case with 'impossible' - we'd be ruling out-    -- too much and wouldn't find the mismatch we're looking for)-    matchingHead apl@(App _ _ _) apr@(App _ _ _)-         | (P _ fl _, argsl) <- unApply apl,-           (P _ fr _, argsr) <- unApply apr,-           isConName fl ctxt && isConName fr ctxt-       = fl == fr-    matchingHead _ _ = True--    -- Return whether there is a possible coercion between the return type-    -- of an alternative and the goal type-    isCoercion rty gty | (P _ r _, _) <- unApply rty-            = not (null (getCoercionsBetween r gty))-    isCoercion _ _ = False--    getCoercionsBetween :: Name -> Type -> [Name]-    getCoercionsBetween r goal-       = let cs = getCoercionsTo ist goal in-             findCoercions r cs-        where findCoercions t [] = []-              findCoercions t (n : ns) =-                 let ps = case lookupTy n (tt_ctxt ist) of-                               [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in-                                            [n | any useR as]-                               _ -> [] in-                     ps ++ findCoercions t ns--              useR ty =-                  case unApply (getRetTy ty) of-                       (P _ t _, _) -> t == r-                       _ -> False---pruneByType _ _ t _ _ as = as---- Could the name feasibly be the return type?--- If there is an interface constraint on the return type, and no implementation--- in the environment or globally for that name, then no--- Otherwise, yes--- (FIXME: This isn't complete, but I'm leaving it here and coming back--- to it later - just returns 'var' for now. EB)-isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool-isPlausible ist var env n ty-    = let (hvar, interfaces) = collectConstraints [] [] ty in-          case hvar of-               Nothing -> True-               Just rth -> var -- trace (show (rth, interfaces)) var-   where-     collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->-                                     (Maybe Name, [(Term, [Name])])-     collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)-         = let tcs' = case unApply ty of-                           (P _ c _, _) ->-                               case lookupCtxtExact c (idris_interfaces ist) of-                                    Just tc -> ((ty, map fst (interface_implementations tc))-                                                     : tcs)-                                    Nothing -> tcs-                           _ -> tcs-                      in-               collectConstraints (n : env) tcs' sc-     collectConstraints env tcs t-         | (V i, _) <- unApply t = (Just (env !! i), tcs)-         | otherwise = (Nothing, tcs)- -- | Use the local elab context to work out the highlighting for a name findHighlight :: Name -> ElabD OutputAnnotation findHighlight n = do ctxt <- get_context@@ -2654,8 +2532,10 @@              letbind scriptvar scriptTy (Var script)              focus script              ptm <- get_term+             env <- get_env+             let denv = map (\(n, _, b) -> (n, binderTy b)) env              elab ist toplevel ERHS [] (sMN 0 "tac")-                  (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True True)])+                  (PApp emptyFC tm [pexp (delabTy' ist [] denv tgoal True True True)])              (script', _) <- get_type_val (Var scriptvar)              -- now that we have the script apply              -- it to the reflected goal
src/Idris/Elab/Utils.hs view
@@ -209,8 +209,11 @@ psolve (Bind n (PVar _ t) sc) = do solve; psolve sc psolve tm = return () -pvars ist (Bind n (PVar _ t) sc) = (n, delab ist t) : pvars ist sc-pvars ist _ = []+pvars ist tm = pv' [] tm+  where+    pv' env (Bind n (PVar _ t) sc)+        = (n, delabWithEnv ist env t) : pv' ((n, t) : env) sc+    pv' env _ = []  getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ _ t _) sc)     = nub $ getFixedInType i env [] t ++@@ -602,5 +605,167 @@ linearArg (Bind n (Pi Rig1 _ _ _) sc) = True linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc linearArg _ = False++-- Rule out alternatives that don't return the same type as the head of the goal+-- (If there are none left as a result, do nothing)+pruneByType :: Bool -> -- In an impossible clause+               Env -> Term -> -- head of the goal+               Type -> -- goal+               IState -> [PTerm] -> [PTerm]+-- if an alternative has a locally bound name at the head, take it+pruneByType imp env t goalty c as+   | Just a <- locallyBound as = [a]+  where+    locallyBound [] = Nothing+    locallyBound (t:ts)+       | Just n <- getName t,+         n `elem` map fstEnv env = Just t+       | otherwise = locallyBound ts+    getName (PRef _ _ n) = Just n+    getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays+       | l == txt "Delay" = getName (getTm arg)+    getName (PApp _ f _) = getName f+    getName (PHidden t) = getName t+    getName _ = Nothing++-- 'n' is the name at the head of the goal type+pruneByType imp env (P _ n _) goalty ist as+-- if the goal type is polymorphic, keep everything+   | Nothing <- lookupTyExact n ctxt = as+-- if the goal type is a ?metavariable, keep everything+   | Just _ <- lookup n (idris_metavars ist) = as+   | otherwise+       = let asV = filter (headIs True n) as+             as' = filter (headIs False n) as in+             case as' of+               [] -> asV+               _ -> as'+  where+    ctxt = tt_ctxt ist++    -- Get the function at the head of the alternative and see if it's+    -- a plausible match against the goal type. Keep if so. Also keep if+    -- there is a possible coercion to the goal type.+    headIs var f (PRef _ _ f') = typeHead var f f'+    headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])+        | l == txt "Delay" = headIs var f (getTm arg)+    headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'+    headIs var f (PApp _ f' _) = headIs var f f'+    headIs var f (PPi _ _ _ _ sc) = headIs var f sc+    headIs var f (PHidden t) = headIs var f t+    headIs var f t = True -- keep if it's not an application++    typeHead var f f'+        = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $+          case lookupTyExact f' ctxt of+               Just ty -> case unApply (getRetTy ty) of+                            (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)+                                     -> False+                            _ -> let ty' = normalise ctxt [] ty in+--                                    trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty+--                                       ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $+                                     case unApply (getRetTy ty') of+                                          (V _, _) ->+                                              isPlausible ist var env n ty+                                          _ -> matchingTypes imp (getRetTy ty') goalty+                                                 || isCoercion (getRetTy ty') goalty+-- May be useful to keep for debugging purposes for a bit:+--                                                let res = matching (getRetTy ty') goalty in+--                                                   traceWhen (not res)+--                                                     ("Rejecting " ++ show (getRetTy ty', goalty)) res+               _ -> False++    matchingTypes True = matchingHead+    matchingTypes False = matching++    -- If the goal is a constructor, it must match the suggested function type+    matching (P _ ctyn _) (P _ n' _)+         | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'+         | otherwise = True+    -- Variables match anything+    matching (V _) _ = True+    matching _ (V _) = True+    matching _ (P _ n _) = not (isTConName n ctxt)+    matching (P _ n _) _ = not (isTConName n ctxt)+    -- Binders are a plausible match, so keep them+    matching (Bind n _ sc) _ = True+    matching _ (Bind n _ sc) = True+    -- If we hit a function name, it's a plausible match+    matching apl@(App _ _ _) apr@(App _ _ _)+         | (P _ fl _, argsl) <- unApply apl,+           (P _ fr _, argsr) <- unApply apr+       = fl == fr && and (zipWith matching argsl argsr)+           || (not (isConName fl ctxt && isConName fr ctxt))+    -- If the application structures aren't easily comparable, it's a+    -- plausible match+    matching (App _ f a) (App _ f' a') = True+    matching (TType _) (TType _) = True+    matching (UType _) (UType _) = True+    matching l r = l == r++    -- In impossible-case mode, only look at the heads (this is to account for+    -- the non type-directed case with 'impossible' - we'd be ruling out+    -- too much and wouldn't find the mismatch we're looking for)+    matchingHead apl@(App _ _ _) apr@(App _ _ _)+         | (P _ fl _, argsl) <- unApply apl,+           (P _ fr _, argsr) <- unApply apr,+           isConName fl ctxt && isConName fr ctxt+       = fl == fr+    matchingHead _ _ = True++    -- Return whether there is a possible coercion between the return type+    -- of an alternative and the goal type+    isCoercion rty gty | (P _ r _, _) <- unApply rty+            = not (null (getCoercionsBetween r gty))+    isCoercion _ _ = False++    getCoercionsBetween :: Name -> Type -> [Name]+    getCoercionsBetween r goal+       = let cs = getCoercionsTo ist goal in+             findCoercions r cs+        where findCoercions t [] = []+              findCoercions t (n : ns) =+                 let ps = case lookupTy n (tt_ctxt ist) of+                               [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in+                                            [n | any useR as]+                               _ -> [] in+                     ps ++ findCoercions t ns++              useR ty =+                  case unApply (getRetTy ty) of+                       (P _ t _, _) -> t == r+                       _ -> False+++pruneByType _ _ t _ _ as = as++-- Could the name feasibly be the return type?+-- If there is an interface constraint on the return type, and no implementation+-- in the environment or globally for that name, then no+-- Otherwise, yes+-- (FIXME: This isn't complete, but I'm leaving it here and coming back+-- to it later - just returns 'var' for now. EB)+isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool+isPlausible ist var env n ty+    = let (hvar, interfaces) = collectConstraints [] [] ty in+          case hvar of+               Nothing -> True+               Just rth -> var -- trace (show (rth, interfaces)) var+   where+     collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->+                                     (Maybe Name, [(Term, [Name])])+     collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)+         = let tcs' = case unApply ty of+                           (P _ c _, _) ->+                               case lookupCtxtExact c (idris_interfaces ist) of+                                    Just tc -> ((ty, map fst (interface_implementations tc))+                                                     : tcs)+                                    Nothing -> tcs+                           _ -> tcs+                      in+               collectConstraints (n : env) tcs' sc+     collectConstraints env tcs t+         | (V i, _) <- unApply t = (Just (env !! i), tcs)+         | otherwise = (Nothing, tcs)
src/Idris/Main.hs view
@@ -37,6 +37,7 @@ import Control.Monad.Trans (lift) import Control.Monad.Trans.Except (runExceptT) import Control.Monad.Trans.State.Strict (execStateT)+import Data.List import Data.Maybe import Prelude hiding (id, (.), (<$>)) import System.Console.Haskeline as H@@ -138,9 +139,21 @@         setNoBanner nobanner +       -- Check if listed packages are actually installed++       idrisCatch (do ipkgs <- runIO $ getIdrisInstalledPackages+                      let diff_pkgs = (\\) pkgdirs ipkgs++                      when (not $ null diff_pkgs) $ do+                        iputStrLn "The following packages were specified but cannot be found:"+                        iputStr $ unlines $ map (\x -> unwords ["-", x]) diff_pkgs+                        runIO $ exitWith (ExitFailure 1))+                  (\e -> return ())+        when (not (NoBasePkgs `elem` opts)) $ do            addPkgDir "prelude"            addPkgDir "base"+        mapM_ addPkgDir pkgdirs        elabPrims        when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)
src/Idris/Output.hs view
@@ -174,6 +174,11 @@                    RawOutput h  -> runIO $ hPutStrLn h s                    IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n +iputStr :: String -> Idris ()+iputStr s = do i <- getIState+               case idris_outputmode i of+                   RawOutput h  -> runIO $ hPutStr h s+                   IdeMode n h -> runIO . hPutStr h $ convSExp "write-string" s n  idemodePutSExp :: SExpable a => String -> a -> Idris () idemodePutSExp cmd info = do i <- getIState
src/Idris/Package.hs view
@@ -499,6 +499,7 @@     chkOpt o@(UseCodegen _)   = Right o     chkOpt o@(Verbose _)      = Right o     chkOpt o@(AuditIPkg)      = Right o+    chkOpt o@(DumpHighlights) = Right o     chkOpt o                  = Left (unwords ["\t", show o, "\n"])      genErrMsg :: [String] -> String@@ -508,6 +509,7 @@         , "\t--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg"         , "\t--ibcsubdir <path>, -i --idrispath <path>"         , "\t--logging-categories <cats>"+        , "\t--highlight"         , "\nThe options need removing are:"         , unlines es         ]
src/Idris/Parser/Data.hs view
@@ -106,7 +106,8 @@                           <|> (symbol "_" >> return Nothing)             ns <- commaSeparated oneName             lchar ':'-            t <- typeExpr (allowImp syn)+            -- Implicits are scoped in fields (fields aren't top level)+            t <- typeExpr (scopedImp syn)             p <- endPlicity c             ist <- get             let doc' = case doc of -- Temp: Throws away any possible arg docs
src/Idris/Parser/Expr.hs view
@@ -46,8 +46,12 @@  -- | Disallow implicit type declarations disallowImp :: SyntaxInfo -> SyntaxInfo-disallowImp syn = syn { implicitAllowed = False,-                        constraintAllowed = False }+disallowImp = scopedImp++-- | Implicits hare are scoped rather than top level+scopedImp :: SyntaxInfo -> SyntaxInfo+scopedImp syn = syn { implicitAllowed = False,+                      constraintAllowed = False }  -- | Allow scoped constraint arguments allowConstr :: SyntaxInfo -> SyntaxInfo
src/Idris/REPL.hs view
@@ -93,6 +93,8 @@ import Util.System import Version_idris (gitHash) +import Debug.Trace+ -- | Run the REPL repl :: IState -- ^ The initial state      -> [FilePath] -- ^ The loaded modules@@ -422,9 +424,9 @@         splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)         splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =           let (hs, c, pc) = splitPi ist (i - 1) rest in-            ((n, t, delabTy' ist [] t False False True):hs,-             c, delabTy' ist [] c False False True)-        splitPi ist i tm = ([], tm, delabTy' ist [] tm False False True)+            ((n, t, delabTy' ist [] [] t False False True):hs,+             c, delabTy' ist [] [] c False False True)+        splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)          -- | Get the types of a list of metavariable names         mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]@@ -1511,15 +1513,16 @@         ppDef amb ist (n, (clauses, missing)) =           prettyName True amb [] n <+> colon <+>           align (pprintDelabTy ist n) <$>-          ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing+          ppClauses ist clauses <> ppMissing missing         ppClauses ist [] = text "No clauses."         ppClauses ist cs = vsep (map pp cs)-          where pp (vars, lhs, rhs) =-                  let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .+          where pp (varTys, lhs, rhs) =+                  let vars = map fst varTys+                      ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .                                pprintPTerm (ppOptionIst ist)                                      (zip vars (repeat False))                                      [] (idris_infixes ist) .-                               delab ist $+                               delabWithEnv ist varTys $                                t                   in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)         ppMissing _ = empty
src/Idris/Termination.hs view
@@ -351,7 +351,8 @@        Delayed <- guarded        -- Under a delayed recursive call just check the arguments            = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args-     | (P _ n _, args) <- unApply ap+     | (P _ n _, args) <- unApply ap,+       not (n `elem` pvs)         -- Ordinary call, not under a delay.         -- If n is a constructor, set 'args' as Guarded         = let nguarded = case guarded of@@ -447,14 +448,17 @@           | otherwise = checkSize a ps       checkSize a [] = Nothing -      -- the smaller thing we find must be defined in the same group of mutally-      -- defined types as <a>, and not be coinductive - so carry the type of-      -- the constructor we've gone under.--      smaller (Just tyn) a (t, Just tyt)-         | a == t = isInductive (fst (unApply (getRetTy tyn)))-                                (fst (unApply (getRetTy tyt)))+      -- Can't be smaller than an erased thing (need to be careful here+      -- because Erased equals everything)+      smaller _ _ (Erased, _) = False -- never smaller than an erased thing+      -- If a == t, and we're under a cosntructor, we've found something+      -- smaller+      smaller (Just tyn) a (t, Just tyt) | a == t = True       smaller ty a (ap@(App _ f s), _)+          -- Nothing can be smaller than a delayed infinite thing...+          | (P (DCon _ _ _) (UN d) _, [P _ (UN reason) _, _, _]) <- unApply ap,+            d == txt "Delay" && reason == txt "Infinite"+               = False           | (P (DCon _ _ _) n _, args) <- unApply ap                = let tyn = getType n in                      any (smaller (ty `mplus` Just tyn) a)@@ -467,13 +471,6 @@        getType n = case lookupTyExact n (tt_ctxt ist) of                        Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist--      isInductive (P _ nty _) (P _ nty' _) =-          let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of-                                [TI _ x _ _ muts _] -> (x, muts)-                                _ -> (False, []) in-              (nty == nty' || any (== nty') muts) && not co-      isInductive _ _ = False    dePat (Bind x (PVar _ ty) sc) = dePat (instantiate (P Bound x ty) sc)   dePat t = t
stack-shell.nix view
@@ -2,7 +2,7 @@  let   # MUST match resolver in stack.yaml-  resolver = haskell.packages.lts-7_19.ghc;+  resolver = haskell.packages.lts-8_4.ghc;    native_libs = [     libffi
stack.yaml view
@@ -1,4 +1,4 @@-resolver: lts-7.19+resolver: lts-8.04  packages:   - location: .
test/TestData.hs view
@@ -77,6 +77,8 @@       (  2, ANY  )]),   ("bounded",         "Bounded",     [ (  1, ANY  )]),+  ("buffer",          "Buffer",+    [ (  1, C_CG  )]),   ("corecords",       "Corecords",     [ (  1, ANY  ),       (  2, ANY  )]),@@ -157,7 +159,7 @@       (  2, ANY  ),       (  3, ANY  ),       (  4, ANY  ),-      (  5, ANY  ),+--       (  5, ANY  ),       (  6, ANY  ),       (  7, ANY  )]),   ("io",              "IO monad",@@ -222,7 +224,8 @@       (  4, ANY  ),       (  5, ANY  )]),   ("reg",             "Regressions",-    [ (  2, ANY  ),+    [ (  1, ANY  ),+      (  2, ANY  ),       (  4, ANY  ),       (  5, ANY  ),       ( 13, ANY  ),@@ -244,7 +247,8 @@       ( 52, C_CG ),       ( 67, ANY  ),       ( 75, ANY  ),-      ( 76, ANY  )]),+      ( 76, ANY  ),+      ( 77, ANY  )]),   ("regression",      "Regression",     [ (  1 , ANY  ),       (  2 , ANY  )]),@@ -281,7 +285,9 @@       ( 17, ANY  ),       ( 18, ANY  ),       ( 19, ANY  ),-      ( 20, ANY  )]),+      ( 20, ANY  ),+      ( 21, ANY  ),+      ( 22, ANY  )]),   ("tutorial",        "Tutorial examples",     [ (  1, ANY  ),       (  2, ANY  ),
test/TestRun.hs view
@@ -108,7 +108,9 @@  main :: IO () main = do-  node <- findExecutable "node"+  nodePath   <- findExecutable "node"+  nodejsPath <- findExecutable "nodejs"+  let node = nodePath <|> nodejsPath   case node of     Nothing -> do       putStrLn "For running the test suite against Node, node must be installed."
+ test/buffer001/buffer001.idr view
@@ -0,0 +1,28 @@+import Data.Buffer++main : IO ()+main = do Just buf <- newBuffer 40+          printLn (size buf)+          setByte buf 5 42+          setString buf 20 "Hello world!"+          printLn !(bufferData buf)+          Just buf2 <- resizeBuffer buf 50 +          putStrLn "Resized"+          printLn !(bufferData buf2)++          putStrLn "Writing to file"+          Right h <- openFile "test.buf" WriteTruncate+          writeBufferToFile h buf (size buf)+          closeFile h++          putStrLn "Reading from file twice"+          Just buf3 <- newBuffer 80++          Right h <- openFile "test.buf" Read+          buf3 <- readBufferFromFile h buf3 (size buf3)+          closeFile h+          Right h <- openFile "test.buf" Read+          readBufferFromFile h buf3 (size buf3)+          closeFile h++          printLn !(bufferData buf3)
+ test/buffer001/expected view
@@ -0,0 +1,7 @@+40+[00, 00, 00, 00, 00, 2A, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, 00, 00, 00, 00]+Resized+[00, 00, 00, 00, 00, 2A, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00]+Writing to file+Reading from file twice+[00, 00, 00, 00, 00, 2A, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 2A, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 00, 48, 65, 6C, 6C, 6F, 20, 77, 6F, 72, 6C, 64, 21, 00, 00, 00, 00, 00, 00, 00, 00]
+ test/buffer001/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ buffer001.idr -o buffer001+./buffer001+rm -f buffer001 test.buf *.ibc
test/interactive010/expected view
@@ -1,6 +1,6 @@ Prelude.List.(++) : List a -> List a -> List a Prelude.Strings.(++) : String -> String -> String-a is not an implicit argument of Prelude.Interfaces./+(input):1:11:a is not an implicit argument of Prelude.Interfaces./ Usage is :doc <functionname> Usage is :wc <functionname> Usage is :printdef <functionname>
test/interfaces005/interfaces005.idr view
@@ -39,15 +39,15 @@ using implementation TreeSet    test : Set Nat-  test = insert 3 $ -         insert 2 $ -         insert 7 $ -         insert 3 $ -         insert 4 $ -         insert 5 new +  test = -- insert (the Nat 3) $ +--          insert 2 $ +--          insert 7 $ +--          insert 3 $ +--          insert 4 $ +        insert {a = Nat} (the Nat 5) new    foo : Bool-  foo = member 6 test+  foo = member (the Nat 6) test    bar : Bool-  bar = member 3 test+  bar = member (the Nat 3) test
test/pkg001/expected view
@@ -4,6 +4,7 @@ 	--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg 	--ibcsubdir <path>, -i --idrispath <path> 	--logging-categories <cats>+	--highlight  The options need removing are: 	 Quiet
test/pkg008/expected view
@@ -11,3 +11,5 @@ Removed: Test.ibc Removed: 00maths-idx.ibc Leaving directory `./src'+The following packages were specified but cannot be found:+- maths
test/pkg008/run view
@@ -7,3 +7,5 @@ # to remove it to make output consistent.  ${IDRIS:-idris} $@ --clean maths.ipkg++${IDRIS:-idris} $@ -p maths
+ test/reg001/Area.idr view
@@ -0,0 +1,12 @@+import TestEx++area : Shape -> Double+area s with (shapeView s)+  area (triangle base height) | STriangle = 0.5 * base * height+  area (rectangle width height) | SRectangle = width * height+  area (circle radius) | SCircle = pi * radius * radius++main : IO ()+main = do printLn (area (rectangle 2 3))+          printLn (area (triangle 2 3))+          printLn (area (circle 1))
+ test/reg001/TestEx.idr view
@@ -0,0 +1,31 @@+module TestEx++export+data Shape = Triangle Double Double+           | Rectangle Double Double+           | Circle Double++export+triangle : Double -> Double -> Shape+triangle = Triangle++export+rectangle : Double -> Double -> Shape+rectangle = Rectangle++export+circle : Double -> Shape+circle = Circle++public export+data ShapeView : Shape -> Type where+     STriangle : ShapeView (triangle base height)+     SRectangle : ShapeView (rectangle width height)+     SCircle : ShapeView (circle radius)++export+shapeView : (s : Shape) -> ShapeView s+shapeView (Triangle x y) = STriangle+shapeView (Rectangle x y) = SRectangle+shapeView (Circle x) = SCircle+
+ test/reg001/expected view
@@ -0,0 +1,3 @@+6+3+3.141592653589793
+ test/reg001/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ Area.idr -o reg001+./reg001+rm -f reg001 *.ibc
+ test/reg077/expected view
+ test/reg077/reg077.idr view
@@ -0,0 +1,17 @@+data Tag : String -> List String -> Type where+  TZ : Tag l (l :: e)+  TS : Tag l e -> Tag l (l' :: e)++SPi :  (e : List String)+    -> ((l : String) -> Tag l e -> Type)+    -> Type+SPi []       _    = ()+SPi (l :: e) prop = (prop l TZ, SPi e $ \l' => \t => prop l' $ TS t)++switch :  (e : List String)+       -> (prop : (l : String) -> (t : Tag l e) -> Type)+       -> SPi e prop+       -> (l' : String) -> (t' : Tag l' e) -> prop l' t'+switch (l' :: e) prop ((propz, props)) l' TZ      = propz+switch (l  :: e) prop ((propz, props)) l' (TS t') =+  switch e (\l => \t => prop l (TS t)) props l' t'
+ test/reg077/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --check reg077.idr+rm -f reg077 *.ibc
+ test/regression001/reg003.idr view
@@ -0,0 +1,11 @@+data Point : Num t => Nat -> t -> Type where+     Nil : Point Z t++data Mono : (Monoid m) => () -> Type where+     Monono : (Monoid m) => Mono {m} ()++data Mono1 : (Monoid m) => Type where+    Monono1 : (Monoid m) => Mono1 {m}++data Mono2 : (m : Type) -> Monoid m => () -> Type where+    Monono2 : (Monoid m) => Mono2 m ()
+ test/regression001/reg004.lidr view
@@ -0,0 +1,43 @@+> %default total+> %access public export+> %auto_implicits off++> Natural : {F, G : Type -> Type} -> +>           (Functor F) => (Functor G) =>+>           (t : {A : Type} -> F A -> G A) -> +>           Type            +> Natural {F} {G} t = {A, B : Type} -> +>                     (f : A -> B) ->+>                     (x : F A) -> +>                     t (map f x) = map f  (t x) ++> Monotone : {B, C : Type} -> {F : Type -> Type} -> (Functor F) => +>            (LTE_B : B -> B -> Type) -> +>            (LTE_C : C -> C -> Type) -> +>            (measure : F B -> C) -> +>            Type+> Monotone {B} {C} {F} LTE_B LTE_C measure =+>   {A : Type} ->+>   (f : A -> B) -> +>   (g : A -> B) -> +>   (p : (a : A) -> f a `LTE_B` g a) -> +>   (x : F A) -> +>   measure (map f x) `LTE_C` measure (map g x)  ++> monotoneNaturalLemma: {B, C : Type} -> {F : Type -> Type} -> (Functor F) => +>                       (LTE_B : B -> B -> Type) -> +>                       (LTE_C : C -> C -> Type) -> +>                       (measure : F B -> C) ->+>                       Monotone LTE_B LTE_C measure -> +>                       (t : {A : Type} -> F A -> F A) -> +>                       Natural t -> +>                       Monotone LTE_B LTE_C (measure . t)+> monotoneNaturalLemma {B} {C} {F} LTE_B LTE_C m mm t nt = mmt where+>   mmt : {A : Type} -> +>         (f : A -> B) -> +>         (g : A -> B) -> +>         (p : (a : A) -> f a `LTE_B` g a) ->+>         (x : F A) -> +>         m (t {A = B} (map f x)) `LTE_C` m (t {A = B} (map g x))   +>   mmt = ?kika+
+ test/regression001/reg005.idr view
@@ -0,0 +1,8 @@+total+map' : (a -> b) -> List a -> List b+map' _ [] = []+map' f (x :: xs) = f x :: map' f xs++f : a+f = f+
+ test/regression001/reg006.idr view
@@ -0,0 +1,14 @@+module Parity++data Parity : Nat -> Type where+   Even : Parity (n + n)+   Odd  : Parity (S (plus n n))++parity : (n:Nat) -> Parity n+parity Z     = Even {n = Z}+parity (S Z) = Odd {n = Z}+parity (S (S k)) with (parity k)+    parity (S (S (j + j)))     | Even +      = rewrite plusSuccRightSucc j j in (Even {n = S j})+    parity (S (S (S (plus j j)))) | Odd+      = rewrite plusSuccRightSucc j j in (Odd {n = S j})
test/regression001/run view
@@ -1,6 +1,7 @@ #!/usr/bin/env bash ${IDRIS:-idris} $@ --check \-    reg001.idr reg002.idr reg036.idr reg037.idr reg038.idr reg046.idr \+    reg001.idr reg002.idr reg003.idr reg004.lidr reg005.idr \+    reg006.idr reg036.idr reg037.idr reg038.idr reg046.idr \     reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \     reg059.idr reg060.idr  reg061.idr reg062.idr reg063.idr \     reg064.idr reg065.idr  reg066.idr reg071.idr reg074.idr \
test/totality020/expected view
@@ -1,1 +1,2 @@ totality020.idr:4:5:bug _ _ Refl is a valid case+totality020.idr:7:5:foo a b Refl is a valid case
test/totality020/totality020.idr view
@@ -2,3 +2,10 @@  bug : (n, m : Nat) -> n + m = n -> Void bug _ _ Refl impossible++foo : (a : Bool) -> (b : Bool) -> Not (const a b = b)+foo a b Refl impossible++myVoid : Void+myVoid = foo True True Refl+
+ test/totality021/expected view
@@ -0,0 +1,9 @@+totality021.idr:8:1:+Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'+totality021.idr:12:1:+Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'+totality021.idr:18:1:Main.v is possibly not total due to: Main.sLevelNotSLevel+totality021a.idr:9:1:+Main.noNonEmptyPointInt is not total as there are missing cases+totality021a.idr:12:1:+Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
+ test/totality021/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ totality021.idr --check+${IDRIS:-idris} $@ totality021a.idr --check+rm -f *.ibc
+ test/totality021/totality021.idr view
@@ -0,0 +1,18 @@+%default total++data Level : Type where+  SL : Inf Level -> Level++sLevelNotSLevel' : (level : Inf Level) ->+                   Not (SL level = SL level)+sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl++sLevelNotSLevel : (level : Level) ->+                  Not (SL (Delay level) = SL (Delay level))+sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl++l : Level+l = SL l++v : Void+v = sLevelNotSLevel l Refl
+ test/totality021/totality021a.idr view
@@ -0,0 +1,12 @@+%default total++-- Testing that overloaded names are properly spotted in impossible cases+data Point : Nat -> t -> Type where+  Nil : Point Z t+  (::) : Num t => t -> Point n t -> Point (S n) t++noNonEmptyPointInt : (Point (S n) Int) -> Void+noNonEmptyPointInt {n} Nil impossible++myVoid : Void+myVoid = noNonEmptyPointInt [2]
+ test/totality022/expected view
@@ -0,0 +1,1 @@+totality022.idr:7:3:f _ [] (RSnoc _ _) is a valid case
+ test/totality022/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ totality022.idr --check+rm -f *.ibc
+ test/totality022/totality022.idr view
@@ -0,0 +1,11 @@+data Rev : List a -> Type where+  RSnoc : (x : a) -> Rev xs -> Rev (xs ++ [x])+  RNil : Rev []++total+f : (x : a) -> (ys : List a) -> (rxs : Rev (ys ++ [x])) -> Void+f _ [] (RSnoc _ _) impossible -- = ?wat+f _ [] RNil impossible+f _ (_ :: _) (RSnoc _ _) impossible+f _ (_ :: _) RNil impossible+