blob: 3a3961fdb669018f6dd359b53c613356acb08c19 (
plain)
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
|
(* Needs ext-lib library to compile. *)
Require Import Coq.ZArith.ZArith_base Coq.Strings.Ascii Coq.Strings.String.
Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
Import StringSyntax.
Open Scope string_scope.
Section StateGame.
Check Ascii.Space.
Import MonadNotation.
Local Open Scope Z_scope.
Local Open Scope char_scope.
Local Open Scope monad_scope.
Definition GameValue : Type := Z.
Definition GameState : Type := (prod bool Z).
Variable m : Type -> Type.
Context {Monad_m: Monad m}.
Context {State_m: MonadState GameState m}.
Print Grammar constr.
Fixpoint playGame (s: string) m' {struct s}: m GameValue :=
match s with
| EmptyString =>
v <- (if true then m' else get) ;;
let '(on, score) := v in ret score
| String x xs =>
v <- get ;;
let '(on, score) := v in
match x, on with
| "a"%char, true => put (on, score + 1)
| "b"%char, true => put (on, score - 1)
| "c"%char, _ => put (negb on, score)
| _, _ => put (on, score)
end ;;
playGame xs m'
end.
Definition startState: GameState := (false, 0).
End StateGame.
|
