git.iko.soy/Idris-dev
on master help sign in
Rename Context->Resources in ST

It's more consistent, and avoids confusion when talking about running in a computation context

commitbce80e0c712ad5c84a69fdbe9b0eebff33754f46 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 20 Mar 2017, 09:57 (10 years ago) parent041b80b
5 files changed+92−29
compare with master
unifiedsplit
docs/image/login.png docs/st/index.rst+23 docs/st/introduction.rst+36 docs/st/machines.rst+4 libs/contrib/Control/ST.idr+29−29
docs/image/login.pngnew file

Binary file not shown.

docs/st/index.rstnew file+23
@@ -0,0 +1,23 @@
1+.. _st-tutorial-index:
2+
3+##########################################################
4+Implementing State-aware Systems in Idris: The ST Tutorial
5+##########################################################
6+
7+A tutorial on implementing state-aware systems using
8+the `Control.ST` library in `Idris`.
9+
10+.. note::
11+
12+ The documentation for Idris has been published under the Creative
13+ Commons CC0 License. As such to the extent possible under law, *The
14+ Idris Community* has waived all copyright and related or neighbouring
15+ rights to Documentation for Idris.
16+
17+ More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
18+
19+.. toctree::
20+ :maxdepth: 1
21+
22+ introduction
23+
docs/st/introduction.rstnew file+36
@@ -0,0 +1,36 @@
1+************
2+Introduction
3+************
4+
5+Pure functional languages with dependent types such as `Idris
6+<http://www.idris-lang.org/>`_ support reasoning about programs directly
7+in the type system, promising that we can *know* a program will run
8+correctly (i.e. according to the specification in its type) simply
9+because it compiles. Realistically, though, things are not so simple:
10+programs have to interact with the outside world, with user input,
11+input from a network, mutable state, and so on.
12+
13+In general, software relies on state, and many components rely on state machines. For
14+example, they describe network transport protocols like TCP, and
15+implement event-driven systems and regular expression matching. Furthermore,
16+many fundamental resources like network sockets and files are, implicitly,
17+managed by state machines, in that certain operations are only valid on
18+resources in certain states, and those operations can change the states of the
19+underlying resource. For example, it only makes sense to send a message on a
20+connected network socket, and closing a socket changes its state from "open" to
21+"closed". State machines can also encode important security properties. For
22+example, in the software which implements an ATM, it’s important that the ATM
23+dispenses cash only when the machine is in a state where a card has been
24+inserted and the PIN verified.
25+
26+In this tutorial I will introduce the `Control.ST` library, which is included
27+with the Idris distribution and supports programming and reasoning with
28+state and side effects.
29+This tutorial assumes familiarity with pure programming in Idris,
30+as described in :ref:`tutorial-index`.
31+
32+The `ST` library allows us to write programs which are composed of multiple
33+state transition systems. It supports composition in two ways: firstly, we can
34+use several independently implemented state transition systems at once;
35+secondly, we can implement one state transition system in terms of others.
36+
docs/st/machines.rstnew file+4
@@ -0,0 +1,4 @@
1+***********************
2+State Machines in Types
3+***********************
4+
libs/contrib/Control/ST.idr+29−29
@@ -20,56 +20,56 @@ export
2020data Var = MkVar -- Phantom, just for labelling purposes
2121
2222{- Contexts for holding current resources states -}
23−namespace Context
23+namespace Resources
2424 public export
25− data Context : Type where
26− Nil : Context
27− (::) : Resource -> Context -> Context
25+ data Resources : Type where
26+ Nil : Resources
27+ (::) : Resource -> Resources -> Resources
2828
2929 public export
30− (++) : Context -> Context -> Context
30+ (++) : Resources -> Resources -> Resources
3131 (++) [] ys = ys
3232 (++) (x :: xs) ys = x :: xs ++ ys
3333
3434{- Proof that a label has a particular type in a given context -}
3535public export
36−data InState : lbl -> Type -> Context -> Type where
36+data InState : lbl -> Type -> Resources -> Type where
3737 Here : InState lbl st (MkRes lbl st :: rs)
3838 There : InState lbl st rs -> InState lbl st (r :: rs)
3939
4040{- Update an entry in a context with a new state -}
4141public export
42−updateCtxt : (ctxt : Context) ->
43− InState lbl st ctxt -> Type -> Context
42+updateCtxt : (ctxt : Resources) ->
43+ InState lbl st ctxt -> Type -> Resources
4444updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
4545updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty
4646
4747{- Remove an entry from a context -}
4848public export
49−drop : (ctxt : Context) -> (prf : InState lbl st ctxt) ->
50− Context
49+drop : (ctxt : Resources) -> (prf : InState lbl st ctxt) ->
50+ Resources
5151drop (MkRes lbl st :: rs) Here = rs
5252drop (r :: rs) (There p) = r :: drop rs p
5353
5454{- Proof that a resource state (label/type) is in a context -}
5555public export
56−data ElemCtxt : Resource -> Context -> Type where
56+data ElemCtxt : Resource -> Resources -> Type where
5757 HereCtxt : ElemCtxt a (a :: as)
5858 ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
5959
6060public export %error_reduce
61−dropEl : (ys: _) -> ElemCtxt x ys -> Context
61+dropEl : (ys: _) -> ElemCtxt x ys -> Resources
6262dropEl (x :: as) HereCtxt = as
6363dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p
6464
6565{- Proof that a variable name is in a context -}
6666public export
67−data VarInCtxt : Var -> Context -> Type where
67+data VarInCtxt : Var -> Resources -> Type where
6868 VarHere : VarInCtxt a (MkRes a st :: as)
6969 VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
7070
7171public export %error_reduce
72−dropVarIn : (ys: _) -> VarInCtxt x ys -> Context
72+dropVarIn : (ys: _) -> VarInCtxt x ys -> Resources
7373dropVarIn ((MkRes x _) :: as) VarHere = as
7474dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
7575
@@ -85,13 +85,13 @@ namespace VarList
8585 (::) : Var -> VarList ts -> VarList (t :: ts)
8686
8787 public export
88− mkCtxt : VarList tys -> Context
88+ mkCtxt : VarList tys -> Resources
8989 mkCtxt [] = []
9090 mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
9191
9292{- Proof that a context is a subset of another context -}
9393public export
94−data SubCtxt : Context -> Context -> Type where
94+data SubCtxt : Resources -> Resources -> Type where
9595 SubNil : SubCtxt [] []
9696 Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
9797 InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
@@ -110,7 +110,7 @@ subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
110110
111111{- Proof that every variable in the list appears once in the context -}
112112public export
113−data VarsIn : List Var -> Context -> Type where
113+data VarsIn : List Var -> Resources -> Type where
114114 VarsNil : VarsIn [] []
115115 SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
116116 InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
@@ -122,8 +122,8 @@ Uninhabited (ElemCtxt x []) where
122122 uninhabited (ThereCtxt _) impossible
123123
124124public export %error_reduce
125−updateWith : (new : Context) -> (xs : Context) ->
126− SubCtxt ys xs -> Context
125+updateWith : (new : Resources) -> (xs : Resources) ->
126+ SubCtxt ys xs -> Resources
127127-- At the end, add the ones which were updated by the subctxt
128128updateWith new [] SubNil = new
129129updateWith new [] (InCtxt el z) = absurd el
@@ -136,7 +136,7 @@ updateWith (n :: ns) (x :: xs) (InCtxt el p)
136136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137137
138138public export
139−getVarType : (xs : Context) -> VarInCtxt v xs -> Type
139+getVarType : (xs : Resources) -> VarInCtxt v xs -> Type
140140getVarType ((MkRes v st) :: as) VarHere = st
141141getVarType (b :: as) (VarThere x) = getVarType as x
142142
@@ -147,20 +147,20 @@ getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y
147147getCombineType (SkipVar x) = getCombineType x
148148
149149public export
150−dropCombined : VarsIn vs ctxt -> Context
150+dropCombined : VarsIn vs ctxt -> Resources
151151dropCombined {ctxt = []} VarsNil = []
152152dropCombined {ctxt} (InCtxtVar el y) = dropCombined y
153153dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x
154154
155155public export
156−combineVarsIn : (ctxt : Context) -> VarsIn (comp :: vs) ctxt -> Context
156+combineVarsIn : (ctxt : Resources) -> VarsIn (comp :: vs) ctxt -> Resources
157157combineVarsIn {comp} ctxt (InCtxtVar el x)
158158 = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))
159159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
160160
161161namespace Env
162162 public export
163− data Env : Context -> Type where
163+ data Env : Resources -> Type where
164164 Nil : Env []
165165 (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
166166
@@ -224,7 +224,7 @@ data Action : Type -> Type where
224224 Stable : lbl -> Type -> Action ty
225225 Trans : lbl -> Type -> (ty -> Type) -> Action ty
226226 Remove : lbl -> Type -> Action ty
227− Add : (ty -> Context) -> Action ty
227+ Add : (ty -> Resources) -> Action ty
228228
229229namespace Stable
230230 public export %error_reduce
@@ -264,7 +264,7 @@ addIfJust : Type -> Action (Maybe a)
264264addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
265265
266266public export
267−kept : SubCtxt xs ys -> Context
267+kept : SubCtxt xs ys -> Resources
268268kept SubNil = []
269269kept (InCtxt el p) = kept p
270270kept (Skip {y} p) = y :: kept p
@@ -279,7 +279,7 @@ data State : Type -> Type where
279279export
280280data STrans : (m : Type -> Type) ->
281281 (ty : Type) ->
282− Context -> (ty -> Context) ->
282+ Resources -> (ty -> Resources) ->
283283 Type where
284284 Pure : (result : ty) ->
285285 STrans m ty (out_fn result) out_fn
@@ -326,7 +326,7 @@ data STrans : (m : Type -> Type) ->
326326namespace Loop
327327 export
328328 data STransLoop : (m : Type -> Type) -> (ty : Type) ->
329− Context -> (ty -> Context) -> Type where
329+ Resources -> (ty -> Resources) -> Type where
330330 Bind : STrans m a st1 st2_fn ->
331331 ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->
332332 STransLoop m b st1 st3_fn
@@ -495,7 +495,7 @@ namespace Loop
495495 pure = Pure
496496
497497public export %error_reduce
498−out_res : ty -> (as : List (Action ty)) -> Context
498+out_res : ty -> (as : List (Action ty)) -> Resources
499499out_res x [] = []
500500out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs
501501out_res x ((Trans lbl inr outr) :: xs)
@@ -504,7 +504,7 @@ out_res x ((Remove lbl inr) :: xs) = out_res x xs
504504out_res x (Add outf :: xs) = outf x ++ out_res x xs
505505
506506public export %error_reduce
507−in_res : (as : List (Action ty)) -> Context
507+in_res : (as : List (Action ty)) -> Resources
508508in_res [] = []
509509in_res ((Stable lbl inr) :: xs) = (lbl ::: inr) :: in_res xs
510510in_res ((Trans lbl inr outr) :: xs) = (lbl ::: inr) :: in_res xs