diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/docs/conf.py b/docs/conf.py --- a/docs/conf.py +++ b/docs/conf.py @@ -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. diff --git a/docs/effects/index.rst b/docs/effects/index.rst --- a/docs/effects/index.rst +++ b/docs/effects/index.rst @@ -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 diff --git a/docs/effects/introduction.rst b/docs/effects/introduction.rst --- a/docs/effects/introduction.rst +++ b/docs/effects/introduction.rst @@ -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: diff --git a/docs/image/login.png b/docs/image/login.png new file mode 100644 Binary files /dev/null and b/docs/image/login.png differ diff --git a/docs/image/netstate.png b/docs/image/netstate.png new file mode 100644 Binary files /dev/null and b/docs/image/netstate.png differ diff --git a/docs/index.rst b/docs/index.rst --- a/docs/index.rst +++ b/docs/index.rst @@ -21,6 +21,7 @@ tutorial/index faq/faq + st/index effects/index proofs/index reference/index diff --git a/docs/listing/idris-prompt-helloworld.txt b/docs/listing/idris-prompt-helloworld.txt --- a/docs/listing/idris-prompt-helloworld.txt +++ b/docs/listing/idris-prompt-helloworld.txt @@ -1,7 +1,7 @@ $ idris hello.idr ____ __ _ / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 0.99.1 + / // __ / ___/ / ___/ Version 0.99.2 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help diff --git a/docs/listing/idris-prompt-interp.txt b/docs/listing/idris-prompt-interp.txt --- a/docs/listing/idris-prompt-interp.txt +++ b/docs/listing/idris-prompt-interp.txt @@ -1,7 +1,7 @@ $ idris interp.idr ____ __ _ / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 0.99.1 + / // __ / ___/ / ___/ Version 0.99.2 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help diff --git a/docs/listing/idris-prompt-start.txt b/docs/listing/idris-prompt-start.txt --- a/docs/listing/idris-prompt-start.txt +++ b/docs/listing/idris-prompt-start.txt @@ -1,7 +1,7 @@ $ idris ____ __ _ / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 0.99.1 + / // __ / ___/ / ___/ Version 0.99.2 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help diff --git a/docs/st/composing.rst b/docs/st/composing.rst new file mode 100644 --- /dev/null +++ b/docs/st/composing.rst @@ -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 diff --git a/docs/st/examples.rst b/docs/st/examples.rst new file mode 100644 --- /dev/null +++ b/docs/st/examples.rst @@ -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 `_ +by Edwin Brady. + +.. |netstate| image:: ../image/netstate.png + :width: 300px + diff --git a/docs/st/index.rst b/docs/st/index.rst new file mode 100644 --- /dev/null +++ b/docs/st/index.rst @@ -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 + diff --git a/docs/st/introduction.rst b/docs/st/introduction.rst new file mode 100644 --- /dev/null +++ b/docs/st/introduction.rst @@ -0,0 +1,93 @@ +******** +Overview +******** + +Pure functional languages with dependent types such as `Idris +`_ 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 `_. + +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 `_, "State Machines All The Way +Down", available `here `_. +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 + + diff --git a/docs/st/machines.rst b/docs/st/machines.rst new file mode 100644 --- /dev/null +++ b/docs/st/machines.rst @@ -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 diff --git a/docs/st/state.rst b/docs/st/state.rst new file mode 100644 --- /dev/null +++ b/docs/st/state.rst @@ -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. + + diff --git a/docs/tutorial/interfaces.rst b/docs/tutorial/interfaces.rst --- a/docs/tutorial/interfaces.rst +++ b/docs/tutorial/interfaces.rst @@ -203,6 +203,8 @@ pure : a -> f a (<*>) : f (a -> b) -> f a -> f b +.. _monadsdo: + Monads and ``do``-notation ========================== diff --git a/docs/tutorial/modules.rst b/docs/tutorial/modules.rst --- a/docs/tutorial/modules.rst +++ b/docs/tutorial/modules.rst @@ -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``, diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -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 diff --git a/libs/base/Control/Catchable.idr b/libs/base/Control/Catchable.idr --- a/libs/base/Control/Catchable.idr +++ b/libs/base/Control/Catchable.idr @@ -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 diff --git a/libs/base/Data/Buffer.idr b/libs/base/Data/Buffer.idr new file mode 100644 --- /dev/null +++ b/libs/base/Data/Buffer.idr @@ -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) diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -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, diff --git a/libs/contrib/Control/ST.idr b/libs/contrib/Control/ST.idr --- a/libs/contrib/Control/ST.idr +++ b/libs/contrib/Control/ST.idr @@ -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) diff --git a/libs/contrib/Control/ST/Exception.idr b/libs/contrib/Control/ST/Exception.idr new file mode 100644 --- /dev/null +++ b/libs/contrib/Control/ST/Exception.idr @@ -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 diff --git a/libs/contrib/Control/ST/ImplicitCall.idr b/libs/contrib/Control/ST/ImplicitCall.idr --- a/libs/contrib/Control/ST/ImplicitCall.idr +++ b/libs/contrib/Control/ST/ImplicitCall.idr @@ -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 diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -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, diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr --- a/libs/prelude/Builtins.idr +++ b/libs/prelude/Builtins.idr @@ -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 diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr --- a/libs/prelude/IO.idr +++ b/libs/prelude/IO.idr @@ -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)) diff --git a/libs/prelude/Prelude/Bits.idr b/libs/prelude/Prelude/Bits.idr --- a/libs/prelude/Prelude/Bits.idr +++ b/libs/prelude/Prelude/Bits.idr @@ -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." diff --git a/libs/prelude/Prelude/File.idr b/libs/prelude/Prelude/File.idr --- a/libs/prelude/Prelude/File.idr +++ b/libs/prelude/Prelude/File.idr @@ -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 diff --git a/libs/prelude/Prelude/Maybe.idr b/libs/prelude/Prelude/Maybe.idr --- a/libs/prelude/Prelude/Maybe.idr +++ b/libs/prelude/Prelude/Maybe.idr @@ -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 diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr --- a/libs/prelude/Prelude/Nat.idr +++ b/libs/prelude/Prelude/Nat.idr @@ -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 diff --git a/libs/prelude/Prelude/Show.idr b/libs/prelude/Prelude/Show.idr --- a/libs/prelude/Prelude/Show.idr +++ b/libs/prelude/Prelude/Show.idr @@ -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 ++ ")" diff --git a/libs/prelude/Prelude/Strings.idr b/libs/prelude/Prelude/Strings.idr --- a/libs/prelude/Prelude/Strings.idr +++ b/libs/prelude/Prelude/Strings.idr @@ -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. diff --git a/man/idris.1 b/man/idris.1 --- a/man/idris.1 +++ b/man/idris.1 @@ -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 diff --git a/rts/Makefile b/rts/Makefile --- a/rts/Makefile +++ b/rts/Makefile @@ -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)\"" diff --git a/rts/idris_buffer.c b/rts/idris_buffer.c new file mode 100644 --- /dev/null +++ b/rts/idris_buffer.c @@ -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); + } +} + diff --git a/rts/idris_buffer.h b/rts/idris_buffer.h new file mode 100644 --- /dev/null +++ b/rts/idris_buffer.h @@ -0,0 +1,23 @@ +#ifndef __BUFFER_H +#define __BUFFER_H + +#include +#include +#include + +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 diff --git a/rts/idris_rts.c b/rts/idris_rts.c --- a/rts/idris_rts.c +++ b/rts/idris_rts.c @@ -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) { diff --git a/rts/idris_rts.h b/rts/idris_rts.h --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -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. diff --git a/rts/idris_stdfgn.c b/rts/idris_stdfgn.c --- a/rts/idris_stdfgn.c +++ b/rts/idris_stdfgn.c @@ -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; +} + diff --git a/rts/idris_stdfgn.h b/rts/idris_stdfgn.h --- a/rts/idris_stdfgn.h +++ b/rts/idris_stdfgn.h @@ -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); diff --git a/rts/idris_utf8.c b/rts/idris_utf8.c --- a/rts/idris_utf8.c +++ b/rts/idris_utf8.c @@ -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; diff --git a/rts/idris_utf8.h b/rts/idris_utf8.h --- a/rts/idris_utf8.h +++ b/rts/idris_utf8.h @@ -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 diff --git a/samples/ST/Composite.idr b/samples/ST/Composite.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Composite.idr @@ -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] diff --git a/samples/ST/Graphics/Draw.idr b/samples/ST/Graphics/Draw.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Graphics/Draw.idr @@ -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 + diff --git a/samples/ST/Graphics/Turtle.idr b/samples/ST/Graphics/Turtle.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Graphics/Turtle.idr @@ -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 + diff --git a/samples/ST/Intro.idr b/samples/ST/Intro.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Intro.idr @@ -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)] + diff --git a/samples/ST/Login.idr b/samples/ST/Login.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Login.idr @@ -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 + diff --git a/samples/ST/LoginCount.idr b/samples/ST/LoginCount.idr new file mode 100644 --- /dev/null +++ b/samples/ST/LoginCount.idr @@ -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) + diff --git a/samples/ST/Net/EchoSimple.idr b/samples/ST/Net/EchoSimple.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Net/EchoSimple.idr @@ -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 + diff --git a/samples/ST/Net/Network.idr b/samples/ST/Net/Network.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Net/Network.idr @@ -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) + diff --git a/samples/ST/Net/RandServer.idr b/samples/ST/Net/RandServer.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Net/RandServer.idr @@ -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 + diff --git a/samples/ST/Net/Threads.idr b/samples/ST/Net/Threads.idr new file mode 100644 --- /dev/null +++ b/samples/ST/Net/Threads.idr @@ -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 () diff --git a/samples/ST/TreeTag.idr b/samples/ST/TreeTag.idr new file mode 100644 --- /dev/null +++ b/samples/ST/TreeTag.idr @@ -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) + + diff --git a/samples/misc/interp.idr b/samples/misc/interp.idr --- a/samples/misc/interp.idr +++ b/samples/misc/interp.idr @@ -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) diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs --- a/src/IRTS/CodegenC.hs +++ b/src/IRTS/CodegenC.hs @@ -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 diff --git a/src/IRTS/CodegenJavaScript.hs b/src/IRTS/CodegenJavaScript.hs --- a/src/IRTS/CodegenJavaScript.hs +++ b/src/IRTS/CodegenJavaScript.hs @@ -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" [ diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -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 diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -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 diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -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 diff --git a/src/Idris/Core/Execute.hs b/src/Idris/Core/Execute.hs --- a/src/Idris/Core/Execute.hs +++ b/src/Idris/Core/Execute.hs @@ -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) = "<>" show (EThunk _ env tm) = "<>" show (EHandle h) = "<>" + show (EStringBuf h) = "<>" 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) diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs --- a/src/Idris/Core/Unify.hs +++ b/src/Idris/Core/Unify.hs @@ -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)] diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs --- a/src/Idris/Coverage.hs +++ b/src/Idris/Coverage.hs @@ -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 diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs --- a/src/Idris/DSL.hs +++ b/src/Idris/DSL.hs @@ -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) diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -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 diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs --- a/src/Idris/Elab/Clause.hs +++ b/src/Idris/Elab/Clause.hs @@ -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) diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs --- a/src/Idris/Elab/Data.hs +++ b/src/Idris/Elab/Data.hs @@ -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 [] diff --git a/src/Idris/Elab/Interface.hs b/src/Idris/Elab/Interface.hs --- a/src/Idris/Elab/Interface.hs +++ b/src/Idris/Elab/Interface.hs @@ -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 diff --git a/src/Idris/Elab/Rewrite.hs b/src/Idris/Elab/Rewrite.hs --- a/src/Idris/Elab/Rewrite.hs +++ b/src/Idris/Elab/Rewrite.hs @@ -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" ++ diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -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 diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs --- a/src/Idris/Elab/Utils.hs +++ b/src/Idris/Elab/Utils.hs @@ -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) diff --git a/src/Idris/Main.hs b/src/Idris/Main.hs --- a/src/Idris/Main.hs +++ b/src/Idris/Main.hs @@ -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) diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs --- a/src/Idris/Output.hs +++ b/src/Idris/Output.hs @@ -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 diff --git a/src/Idris/Package.hs b/src/Idris/Package.hs --- a/src/Idris/Package.hs +++ b/src/Idris/Package.hs @@ -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 , --total, --warnpartial, --warnreach, --warnipkg" , "\t--ibcsubdir , -i --idrispath " , "\t--logging-categories " + , "\t--highlight" , "\nThe options need removing are:" , unlines es ] diff --git a/src/Idris/Parser/Data.hs b/src/Idris/Parser/Data.hs --- a/src/Idris/Parser/Data.hs +++ b/src/Idris/Parser/Data.hs @@ -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 diff --git a/src/Idris/Parser/Expr.hs b/src/Idris/Parser/Expr.hs --- a/src/Idris/Parser/Expr.hs +++ b/src/Idris/Parser/Expr.hs @@ -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 diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -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 diff --git a/src/Idris/Termination.hs b/src/Idris/Termination.hs --- a/src/Idris/Termination.hs +++ b/src/Idris/Termination.hs @@ -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 , 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 diff --git a/stack-shell.nix b/stack-shell.nix --- a/stack-shell.nix +++ b/stack-shell.nix @@ -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 diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-7.19 +resolver: lts-8.04 packages: - location: . diff --git a/test/TestData.hs b/test/TestData.hs --- a/test/TestData.hs +++ b/test/TestData.hs @@ -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 ), diff --git a/test/TestRun.hs b/test/TestRun.hs --- a/test/TestRun.hs +++ b/test/TestRun.hs @@ -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." diff --git a/test/buffer001/buffer001.idr b/test/buffer001/buffer001.idr new file mode 100644 --- /dev/null +++ b/test/buffer001/buffer001.idr @@ -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) diff --git a/test/buffer001/expected b/test/buffer001/expected new file mode 100644 --- /dev/null +++ b/test/buffer001/expected @@ -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] diff --git a/test/buffer001/run b/test/buffer001/run new file mode 100644 --- /dev/null +++ b/test/buffer001/run @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ buffer001.idr -o buffer001 +./buffer001 +rm -f buffer001 test.buf *.ibc diff --git a/test/interactive010/expected b/test/interactive010/expected --- a/test/interactive010/expected +++ b/test/interactive010/expected @@ -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 Usage is :wc Usage is :printdef diff --git a/test/interfaces005/interfaces005.idr b/test/interfaces005/interfaces005.idr --- a/test/interfaces005/interfaces005.idr +++ b/test/interfaces005/interfaces005.idr @@ -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 diff --git a/test/pkg001/expected b/test/pkg001/expected --- a/test/pkg001/expected +++ b/test/pkg001/expected @@ -4,6 +4,7 @@ --log , --total, --warnpartial, --warnreach, --warnipkg --ibcsubdir , -i --idrispath --logging-categories + --highlight The options need removing are: Quiet diff --git a/test/pkg008/expected b/test/pkg008/expected --- a/test/pkg008/expected +++ b/test/pkg008/expected @@ -11,3 +11,5 @@ Removed: Test.ibc Removed: 00maths-idx.ibc Leaving directory `./src' +The following packages were specified but cannot be found: +- maths diff --git a/test/pkg008/run b/test/pkg008/run --- a/test/pkg008/run +++ b/test/pkg008/run @@ -7,3 +7,5 @@ # to remove it to make output consistent. ${IDRIS:-idris} $@ --clean maths.ipkg + +${IDRIS:-idris} $@ -p maths diff --git a/test/reg001/Area.idr b/test/reg001/Area.idr new file mode 100644 --- /dev/null +++ b/test/reg001/Area.idr @@ -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)) diff --git a/test/reg001/TestEx.idr b/test/reg001/TestEx.idr new file mode 100644 --- /dev/null +++ b/test/reg001/TestEx.idr @@ -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 + diff --git a/test/reg001/expected b/test/reg001/expected new file mode 100644 --- /dev/null +++ b/test/reg001/expected @@ -0,0 +1,3 @@ +6 +3 +3.141592653589793 diff --git a/test/reg001/run b/test/reg001/run new file mode 100644 --- /dev/null +++ b/test/reg001/run @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ Area.idr -o reg001 +./reg001 +rm -f reg001 *.ibc diff --git a/test/reg077/expected b/test/reg077/expected new file mode 100644 --- /dev/null +++ b/test/reg077/expected diff --git a/test/reg077/reg077.idr b/test/reg077/reg077.idr new file mode 100644 --- /dev/null +++ b/test/reg077/reg077.idr @@ -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' diff --git a/test/reg077/run b/test/reg077/run new file mode 100644 --- /dev/null +++ b/test/reg077/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ --check reg077.idr +rm -f reg077 *.ibc diff --git a/test/regression001/reg003.idr b/test/regression001/reg003.idr new file mode 100644 --- /dev/null +++ b/test/regression001/reg003.idr @@ -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 () diff --git a/test/regression001/reg004.lidr b/test/regression001/reg004.lidr new file mode 100644 --- /dev/null +++ b/test/regression001/reg004.lidr @@ -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 + diff --git a/test/regression001/reg005.idr b/test/regression001/reg005.idr new file mode 100644 --- /dev/null +++ b/test/regression001/reg005.idr @@ -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 + diff --git a/test/regression001/reg006.idr b/test/regression001/reg006.idr new file mode 100644 --- /dev/null +++ b/test/regression001/reg006.idr @@ -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}) diff --git a/test/regression001/run b/test/regression001/run --- a/test/regression001/run +++ b/test/regression001/run @@ -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 \ diff --git a/test/totality020/expected b/test/totality020/expected --- a/test/totality020/expected +++ b/test/totality020/expected @@ -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 diff --git a/test/totality020/totality020.idr b/test/totality020/totality020.idr --- a/test/totality020/totality020.idr +++ b/test/totality020/totality020.idr @@ -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 + diff --git a/test/totality021/expected b/test/totality021/expected new file mode 100644 --- /dev/null +++ b/test/totality021/expected @@ -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 diff --git a/test/totality021/run b/test/totality021/run new file mode 100644 --- /dev/null +++ b/test/totality021/run @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ totality021.idr --check +${IDRIS:-idris} $@ totality021a.idr --check +rm -f *.ibc diff --git a/test/totality021/totality021.idr b/test/totality021/totality021.idr new file mode 100644 --- /dev/null +++ b/test/totality021/totality021.idr @@ -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 diff --git a/test/totality021/totality021a.idr b/test/totality021/totality021a.idr new file mode 100644 --- /dev/null +++ b/test/totality021/totality021a.idr @@ -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] diff --git a/test/totality022/expected b/test/totality022/expected new file mode 100644 --- /dev/null +++ b/test/totality022/expected @@ -0,0 +1,1 @@ +totality022.idr:7:3:f _ [] (RSnoc _ _) is a valid case diff --git a/test/totality022/run b/test/totality022/run new file mode 100644 --- /dev/null +++ b/test/totality022/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ totality022.idr --check +rm -f *.ibc diff --git a/test/totality022/totality022.idr b/test/totality022/totality022.idr new file mode 100644 --- /dev/null +++ b/test/totality022/totality022.idr @@ -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 +