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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
set show timing off .
set show advisories off .
***
*** Strategy modules, theories and views
***
sth STRIV is
including TRIV .
strat stt @ Elt .
endsth
mod FOO is
protecting QID .
var X : Qid .
rl [rh] : X => qid("h" + string(X)) .
endm
view Foo from STRIV to FOO is
sort Elt to Qid .
strat stt to expr rh .
endv
smod REPEAT{X :: STRIV} is
protecting NAT .
var N : Nat .
strat repeat : Nat @ X$Elt .
sd repeat(0) := idle .
sd repeat(s(N)) := stt ; repeat(N) .
endsm
smod BAR is
protecting REPEAT{Foo} * (strat repeat to puths) .
endsm
show all .
srew 'a using puths(8) .
view STriv from TRIV to STRIV is
endv
smod PROMOTED is
protecting LIST{STriv}{Foo} .
endsm
red 'a 'b 'c .
***
*** Strategy calls and traces
***
smod CALLS is
protecting FOO .
protecting SET{Qid} .
strat cond @ Qid . *** different matches from the assignement condition
strat defs @ Qid . *** different matches from different definitions
strat args : Set{Qid} @ Qid . *** different matches from the argument
var X : Qid .
var S : Set{Qid} .
csd cond := rh[X <- X] if X, S := 'a, 'b, 'c .
sd defs := fail .
sd defs := rh .
sd defs := idle .
sd args((X, S)) := rh[X <- X] .
endsm
set trace eq off .
set trace rl off .
set trace whole on .
set trace on .
srew 'c using cond .
srew 'b using defs .
srew 'a using args(('a, 'z)) .
set trace sd off .
set trace off .
***
*** Detection of some bad strategy terms
***
smod BAD is
protecting FOO .
var Q R : Qid .
strat st @ Qid .
strat st : Qid @ Qid .
csd st := idle if Q = 'a .
sd st := rh[Q <- Q] .
sd st := match R s.t. Q == R .
sd st := st(Q) .
endsm
***
*** Strategy modules containing rules and equations
***
smod ALLINSMOD is
sorts Letter Vowel .
subsort Vowel < Letter .
ops b c d : -> Letter .
ops a e i o u : -> Vowel .
op next : Letter -> Letter .
eq next(a) = b .
eq next(b) = c .
var L : Letter .
rl [next] : L => next(L) .
strat next @ Letter .
sd next() := next ; next .
endsm
srew a using next .
srew a using next() .
|
