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
|
set show timing off .
set show advisories off .
***
*** Check that mb applications and eq rewrites for the initial
*** sort computations in the subject are not counted twice for
*** metaMatch()/metaXmatch()/getMatch()/getXmatch().
***
fmod MATCH is
sorts Foo Bar .
subsorts Foo < Bar .
op f : Bar Bar -> Bar [comm] .
ops g h : Foo -> Foo .
ops a b c d e : -> Foo .
vars X Y : Bar .
var Z : Foo .
cmb f(X, Y) : Foo if h(X) = g(Y) .
eq h(a) = b .
eq g(c) = b .
eq h(c) = d .
eq g(a) = d .
endfm
set trace on .
set show breakdown on .
red in META-LEVEL : metaMatch(['MATCH], 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, 0) .
red in META-LEVEL : metaXmatch(['MATCH], 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, 0, unbounded, 0) .
load metaInterpreter
mod MATCH-TEST is
pr META-INTERPRETER .
op me : -> Oid .
op User : -> Cid .
op soln:_ : Nat -> Attribute .
vars X Y Z : Oid .
var AS : AttributeSet .
var N : Nat .
rl < X : User | AS > createdInterpreter(X, Y, Z) =>
< X : User | AS > insertModule(Z, X, upModule('MATCH, true)) .
rl < X : User | soln: N, AS > insertedModule(X, Y) =>
< X : User | AS > getMatch(Y, X, 'MATCH, 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, N) .
endm
erew in MATCH-TEST : <>
< me : User | soln: 0 >
createInterpreter(interpreterManager, me, none) .
mod XMATCH-TEST is
pr META-INTERPRETER .
op me : -> Oid .
op User : -> Cid .
op soln:_ : Nat -> Attribute .
vars X Y Z : Oid .
var AS : AttributeSet .
var N : Nat .
rl < X : User | AS > createdInterpreter(X, Y, Z) =>
< X : User | AS > insertModule(Z, X, upModule('MATCH, true)) .
rl < X : User | soln: N, AS > insertedModule(X, Y) =>
< X : User | AS > getXmatch(Y, X, 'MATCH, 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, 0, unbounded, N) .
endm
erew in XMATCH-TEST : <>
< me : User | soln: 0 >
createInterpreter(interpreterManager, me, none) .
|
