1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
(** Non-termination and state monad with extraction *)
Require Import TestSuite.list.
Set Implicit Arguments.
Set Asymmetric Patterns.
Module MemSig.
Definition t: Type := list Type.
Definition Nth (sig: t) (n: nat) :=
nth n sig unit.
End MemSig.
(** A memory of type [Mem.t s] is the union of cells whose type is specified
by [s]. *)
Module Mem.
Inductive t: MemSig.t -> Type :=
| Nil: t nil
| Cons: forall (T: Type), option T -> forall (sig: MemSig.t), t sig ->
t (cons T sig).
End Mem.
Module Ref.
Inductive t (sig: MemSig.t) (T: Type): Type :=
| Input: t sig T.
Definition Read (sig: MemSig.t) (T: Type) (ref: t sig T) (s: Mem.t sig)
: option T :=
match ref with
| Input => None
end.
End Ref.
Module Monad.
Definition t (sig: MemSig.t) (A: Type) :=
Mem.t sig -> option A * Mem.t sig.
Definition Return (sig: MemSig.t) (A: Type) (x: A): t sig A :=
fun s =>
(Some x, s).
Definition Bind (sig: MemSig.t) (A B: Type) (x: t sig A) (f: A -> t sig B)
: t sig B :=
fun s =>
match x s with
| (Some x', s') => f x' s'
| (None, s') => (None, s')
end.
Definition Select (T: Type) (f g: unit -> T): T :=
f tt.
(** Read in a reference. *)
Definition Read (sig: MemSig.t) (T: Type) (ref: Ref.t sig T)
: t sig T :=
fun s =>
match Ref.Read ref s with
| None => (None, s)
| Some x => (Some x, s)
end.
End Monad.
Import Monad.
Definition pop (sig: MemSig.t) (T: Type) (trace: Ref.t sig (list T))
: Monad.t sig T :=
Bind (Read trace) (fun _ s => (None, s)).
Definition sig: MemSig.t := cons (list nat: Type) nil.
Definition trace: Ref.t sig (list nat).
Admitted.
Definition Gre (sig: MemSig.t) (trace: _)
(f: bool -> bool): Monad.t sig nat :=
Select (fun _ => pop trace) (fun _ => Return 0).
Definition Arg :=
Gre trace (fun _ => false).
|
