git.iko.soy/Idris-dev
on master help sign in
Rename Context->Resources in ST
bce80e0Edwin Brady
docs/image/login.pngnew file
compare with master
unifiedsplit

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
20data Var = MkVar -- Phantom, just for labelling purposes
20data Var = MkVar -- Phantom, just for labelling purposes
21
21
22{- Contexts for holding current resources states -}
22{- Contexts for holding current resources states -}
23−namespace Context
23+namespace Resources
24 public export
24 public export
25− data Context : Type where
25+ data Resources : Type where
26− Nil : Context
26+ Nil : Resources
27− (::) : Resource -> Context -> Context
27+ (::) : Resource -> Resources -> Resources
28
28
29 public export
29 public export
30− (++) : Context -> Context -> Context
30+ (++) : Resources -> Resources -> Resources
31 (++) [] ys = ys
31 (++) [] ys = ys
32 (++) (x :: xs) ys = x :: xs ++ ys
32 (++) (x :: xs) ys = x :: xs ++ ys
33
33
34{- Proof that a label has a particular type in a given context -}
34{- Proof that a label has a particular type in a given context -}
35public export
35public export
36−data InState : lbl -> Type -> Context -> Type where
36+data InState : lbl -> Type -> Resources -> Type where
37 Here : InState lbl st (MkRes lbl st :: rs)
37 Here : InState lbl st (MkRes lbl st :: rs)
38 There : InState lbl st rs -> InState lbl st (r :: rs)
38 There : InState lbl st rs -> InState lbl st (r :: rs)
39
39
40{- Update an entry in a context with a new state -}
40{- Update an entry in a context with a new state -}
41public export
41public export
42−updateCtxt : (ctxt : Context) ->
42+updateCtxt : (ctxt : Resources) ->
43− InState lbl st ctxt -> Type -> Context
43+ InState lbl st ctxt -> Type -> Resources
44updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
44updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
45updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty
45updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty
46
46
47{- Remove an entry from a context -}
47{- Remove an entry from a context -}
48public export
48public export
49−drop : (ctxt : Context) -> (prf : InState lbl st ctxt) ->
49+drop : (ctxt : Resources) -> (prf : InState lbl st ctxt) ->
50− Context
50+ Resources
51drop (MkRes lbl st :: rs) Here = rs
51drop (MkRes lbl st :: rs) Here = rs
52drop (r :: rs) (There p) = r :: drop rs p
52drop (r :: rs) (There p) = r :: drop rs p
53
53
54{- Proof that a resource state (label/type) is in a context -}
54{- Proof that a resource state (label/type) is in a context -}
55public export
55public export
56−data ElemCtxt : Resource -> Context -> Type where
56+data ElemCtxt : Resource -> Resources -> Type where
57 HereCtxt : ElemCtxt a (a :: as)
57 HereCtxt : ElemCtxt a (a :: as)
58 ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
58 ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
59
59
60public export %error_reduce
60public export %error_reduce
61−dropEl : (ys: _) -> ElemCtxt x ys -> Context
61+dropEl : (ys: _) -> ElemCtxt x ys -> Resources
62dropEl (x :: as) HereCtxt = as
62dropEl (x :: as) HereCtxt = as
63dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p
63dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p
64
64
65{- Proof that a variable name is in a context -}
65{- Proof that a variable name is in a context -}
66public export
66public export
67−data VarInCtxt : Var -> Context -> Type where
67+data VarInCtxt : Var -> Resources -> Type where
68 VarHere : VarInCtxt a (MkRes a st :: as)
68 VarHere : VarInCtxt a (MkRes a st :: as)
69 VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
69 VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
70
70
71public export %error_reduce
71public export %error_reduce
72−dropVarIn : (ys: _) -> VarInCtxt x ys -> Context
72+dropVarIn : (ys: _) -> VarInCtxt x ys -> Resources
73dropVarIn ((MkRes x _) :: as) VarHere = as
73dropVarIn ((MkRes x _) :: as) VarHere = as
74dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
74dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
75
75
@@ -85,13 +85,13 @@ namespace VarList
85 (::) : Var -> VarList ts -> VarList (t :: ts)
85 (::) : Var -> VarList ts -> VarList (t :: ts)
86
86
87 public export
87 public export
88− mkCtxt : VarList tys -> Context
88+ mkCtxt : VarList tys -> Resources
89 mkCtxt [] = []
89 mkCtxt [] = []
90 mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
90 mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
91
91
92{- Proof that a context is a subset of another context -}
92{- Proof that a context is a subset of another context -}
93public export
93public export
94−data SubCtxt : Context -> Context -> Type where
94+data SubCtxt : Resources -> Resources -> Type where
95 SubNil : SubCtxt [] []
95 SubNil : SubCtxt [] []
96 Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
96 Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
97 InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
97 InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
@@ -110,7 +110,7 @@ subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
110
110
111{- Proof that every variable in the list appears once in the context -}
111{- Proof that every variable in the list appears once in the context -}
112public export
112public export
113−data VarsIn : List Var -> Context -> Type where
113+data VarsIn : List Var -> Resources -> Type where
114 VarsNil : VarsIn [] []
114 VarsNil : VarsIn [] []
115 SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
115 SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
116 InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116 InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
@@ -122,8 +122,8 @@ Uninhabited (ElemCtxt x []) where
122 uninhabited (ThereCtxt _) impossible
122 uninhabited (ThereCtxt _) impossible
123
123
124public export %error_reduce
124public export %error_reduce
125−updateWith : (new : Context) -> (xs : Context) ->
125+updateWith : (new : Resources) -> (xs : Resources) ->
126− SubCtxt ys xs -> Context
126+ SubCtxt ys xs -> Resources
127-- At the end, add the ones which were updated by the subctxt
127-- At the end, add the ones which were updated by the subctxt
128updateWith new [] SubNil = new
128updateWith new [] SubNil = new
129updateWith new [] (InCtxt el z) = absurd el
129updateWith new [] (InCtxt el z) = absurd el
@@ -136,7 +136,7 @@ updateWith (n :: ns) (x :: xs) (InCtxt el p)
136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137
137
138public export
138public export
139−getVarType : (xs : Context) -> VarInCtxt v xs -> Type
139+getVarType : (xs : Resources) -> VarInCtxt v xs -> Type
140getVarType ((MkRes v st) :: as) VarHere = st
140getVarType ((MkRes v st) :: as) VarHere = st
141getVarType (b :: as) (VarThere x) = getVarType as x
141getVarType (b :: as) (VarThere x) = getVarType as x
142
142
@@ -147,20 +147,20 @@ getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y
147getCombineType (SkipVar x) = getCombineType x
147getCombineType (SkipVar x) = getCombineType x
148
148
149public export
149public export
150−dropCombined : VarsIn vs ctxt -> Context
150+dropCombined : VarsIn vs ctxt -> Resources
151dropCombined {ctxt = []} VarsNil = []
151dropCombined {ctxt = []} VarsNil = []
152dropCombined {ctxt} (InCtxtVar el y) = dropCombined y
152dropCombined {ctxt} (InCtxtVar el y) = dropCombined y
153dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x
153dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x
154
154
155public export
155public export
156−combineVarsIn : (ctxt : Context) -> VarsIn (comp :: vs) ctxt -> Context
156+combineVarsIn : (ctxt : Resources) -> VarsIn (comp :: vs) ctxt -> Resources
157combineVarsIn {comp} ctxt (InCtxtVar el x)
157combineVarsIn {comp} ctxt (InCtxtVar el x)
158 = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))
158 = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))
159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
160
160
161namespace Env
161namespace Env
162 public export
162 public export
163− data Env : Context -> Type where
163+ data Env : Resources -> Type where
164 Nil : Env []
164 Nil : Env []
165 (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
165 (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
166
166
@@ -224,7 +224,7 @@ data Action : Type -> Type where
224 Stable : lbl -> Type -> Action ty
224 Stable : lbl -> Type -> Action ty
225 Trans : lbl -> Type -> (ty -> Type) -> Action ty
225 Trans : lbl -> Type -> (ty -> Type) -> Action ty
226 Remove : lbl -> Type -> Action ty
226 Remove : lbl -> Type -> Action ty
227− Add : (ty -> Context) -> Action ty
227+ Add : (ty -> Resources) -> Action ty
228
228
229namespace Stable
229namespace Stable
230 public export %error_reduce
230 public export %error_reduce
@@ -264,7 +264,7 @@ addIfJust : Type -> Action (Maybe a)
264addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
264addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
265
265
266public export
266public export
267−kept : SubCtxt xs ys -> Context
267+kept : SubCtxt xs ys -> Resources
268kept SubNil = []
268kept SubNil = []
269kept (InCtxt el p) = kept p
269kept (InCtxt el p) = kept p
270kept (Skip {y} p) = y :: kept p
270kept (Skip {y} p) = y :: kept p
@@ -279,7 +279,7 @@ data State : Type -> Type where
279export
279export
280data STrans : (m : Type -> Type) ->
280data STrans : (m : Type -> Type) ->
281 (ty : Type) ->
281 (ty : Type) ->
282− Context -> (ty -> Context) ->
282+ Resources -> (ty -> Resources) ->
283 Type where
283 Type where
284 Pure : (result : ty) ->
284 Pure : (result : ty) ->
285 STrans m ty (out_fn result) out_fn
285 STrans m ty (out_fn result) out_fn
@@ -326,7 +326,7 @@ data STrans : (m : Type -> Type) ->
326namespace Loop
326namespace Loop
327 export
327 export
328 data STransLoop : (m : Type -> Type) -> (ty : Type) ->
328 data STransLoop : (m : Type -> Type) -> (ty : Type) ->
329− Context -> (ty -> Context) -> Type where
329+ Resources -> (ty -> Resources) -> Type where
330 Bind : STrans m a st1 st2_fn ->
330 Bind : STrans m a st1 st2_fn ->
331 ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->
331 ((result : a) -> Inf (STransLoop m b (st2_fn result) st3_fn)) ->
332 STransLoop m b st1 st3_fn
332 STransLoop m b st1 st3_fn
@@ -495,7 +495,7 @@ namespace Loop
495 pure = Pure
495 pure = Pure
496
496
497public export %error_reduce
497public export %error_reduce
498−out_res : ty -> (as : List (Action ty)) -> Context
498+out_res : ty -> (as : List (Action ty)) -> Resources
499out_res x [] = []
499out_res x [] = []
500out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs
500out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs
501out_res x ((Trans lbl inr outr) :: xs)
501out_res x ((Trans lbl inr outr) :: xs)
@@ -504,7 +504,7 @@ out_res x ((Remove lbl inr) :: xs) = out_res x xs
504out_res x (Add outf :: xs) = outf x ++ out_res x xs
504out_res x (Add outf :: xs) = outf x ++ out_res x xs
505
505
506public export %error_reduce
506public export %error_reduce
507−in_res : (as : List (Action ty)) -> Context
507+in_res : (as : List (Action ty)) -> Resources
508in_res [] = []
508in_res [] = []
509in_res ((Stable lbl inr) :: xs) = (lbl ::: inr) :: in_res xs
509in_res ((Stable lbl inr) :: xs) = (lbl ::: inr) :: in_res xs
510in_res ((Trans lbl inr outr) :: xs) = (lbl ::: inr) :: in_res xs
510in_res ((Trans lbl inr outr) :: xs) = (lbl ::: inr) :: in_res xs