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
|
==========================================
reduce in TEST : g(X:Foo) .
rewrites: 1
result Foo: h(h(X:Foo, c), c)
==========================================
reduce in META1 : T .
rewrites: 2
result FTheory: fth 'T is
nil
sorts 'Elt .
none
op 'f : 'Elt -> 'Elt [none] .
none
none
endfth
==========================================
reduce in META1 : M .
rewrites: 2
result FModule: fmod 'M{'X :: 'T} is
nil
sorts none .
none
op 'g : 'X$Elt -> 'X$Elt [none] .
none
eq 'g['X:X$Elt] = 'f['f['X:X$Elt]] [none] .
endfm
==========================================
reduce in META1 : FOO .
rewrites: 2
result FModule: fmod 'FOO is
nil
sorts 'Foo .
none
op 'c : nil -> 'Foo [none] .
op 'h : 'Foo 'Foo -> 'Foo [none] .
none
none
endfm
==========================================
reduce in META1 : V .
rewrites: 2
result View: view 'V from 'T to 'FOO is
sort 'Elt to 'Foo .
op 'f['X:Elt] to term 'h['X:Foo, 'c.Foo] .
none
endv
==========================================
reduce in META1 : TEST .
rewrites: 2
result FModule: fmod 'TEST is
including 'M{'V} .
sorts none .
none
none
none
none
endfm
==========================================
erewrite in META2 : <> < me : User | state: 1 > createInterpreter(
interpreterManager, me, none) .
rewrites: 17
result Configuration: <> < me : User | state: 7 > reducedTerm(me, interpreter(
0), 1, 'h['h['X:Foo, 'c.Foo], 'c.Foo], 'Foo)
==========================================
erewrite in META3 : <> < me : User | state: 1 > createInterpreter(
interpreterManager, me, none) .
rewrites: 21
result Configuration: <> < me : User | state: 9 > reducedTerm(me, interpreter(
0), 1, 'h['h['h['X:Foo, 'c.Foo], 'c.Foo], 'c.Foo], 'Foo)
==========================================
erewrite in META4 : <> < me : User | state: 1 > createInterpreter(
interpreterManager, me, none) .
rewrites: 21
result Configuration: <> < me : User | state: 9 > reducedTerm(me, interpreter(
0), 1, 'h['c.Foo, 'h['c.Foo, 'X:Foo]], 'Foo)
==========================================
erewrite in META5 : <> < me : User | state: 1 > createInterpreter(
interpreterManager, me, none) .
rewrites: 23
result Configuration: <> < me : User | state: 10 > reducedTerm(me, interpreter(
0), 1, 'k['k['X:Foo, 'd.Foo], 'd.Foo], 'Foo)
Bye.
|
