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
130
131
132
133
134
135
136
137
138
139
|
fmod FOO is
sort Foo .
ops a b : -> Foo [metadata "bla bla"] .
eq a = b [metadata "hmm"] .
endfm
fmod FOO is
sort Foo .
op a : -> Foo [metadata "bla bla"] .
op b : -> Foo [metadata "bla bla"] .
eq a = b [metadata "hmm"] .
endfm
==========================================
reduce in META-LEVEL : upModule('FOO, false) .
rewrites: 1
result FModule: fmod 'FOO is
nil
sorts 'Foo .
none
op 'a : nil -> 'Foo [metadata("bla bla")] .
op 'b : nil -> 'Foo [metadata("bla bla")] .
none
eq 'a.Foo = 'b.Foo [metadata("hmm")] .
endfm
Warning: <standard input>, line 19 (fmod FOO2): bad value bla for metadata
attribute.
Warning: <standard input>, line 20 (fmod FOO2): bad token hmm.
Warning: <standard input>, line 20 (fmod FOO2): no parse for statement
eq a = b [metadata hmm] .
fmod FOO2 is
sort Foo .
ops a b : -> Foo .
eq a = b [metadata hmm] .
endfm
fmod FOO2 is
sort Foo .
op a : -> Foo .
op b : -> Foo .
endfm
==========================================
reduce in META-LEVEL : upModule('FOO, false) .
rewrites: 1
result FModule: fmod 'FOO is
nil
sorts 'Foo .
none
op 'a : nil -> 'Foo [metadata("bla bla")] .
op 'b : nil -> 'Foo [metadata("bla bla")] .
none
eq 'a.Foo = 'b.Foo [metadata("hmm")] .
endfm
fmod FOO3 is
sort Foo .
op a : -> Foo [metadata "bla bla"] .
op b : -> Foo [metadata "bla bla"] .
eq a = b [metadata "hmm"] .
endfm
==========================================
reduce in META-LEVEL : upModule('FOO3, true) .
rewrites: 1
result FModule: fmod 'FOO3 is
nil
sorts 'Foo .
none
op 'a : nil -> 'Foo [metadata("bla bla")] .
op 'b : nil -> 'Foo [metadata("bla bla")] .
none
eq 'a.Foo = 'b.Foo [metadata("hmm")] .
endfm
fmod FOO4 is
sort Foo .
op f : ??? -> Foo [poly (1) metadata "bla bla"] .
endfm
fmod FOO4 is
sort Foo .
op f : Universal -> Foo [poly (1) metadata "bla bla"] .
endfm
==========================================
reduce in META-LEVEL : upModule('FOO4, false) .
rewrites: 1
result FModule: fmod 'FOO4 is
nil
sorts 'Foo .
none
op 'f : 'Universal -> 'Foo [poly(1) metadata("bla bla")] .
none
none
endfm
fmod FOO5 is
sort Foo .
op f : Universal -> Foo [poly (1) metadata "bla bla"] .
endfm
==========================================
reduce in META-LEVEL : upModule('FOO5, true) .
rewrites: 1
result FModule: fmod 'FOO5 is
nil
sorts 'Foo .
none
op 'f : 'Universal -> 'Foo [poly(1) metadata("bla bla")] .
none
none
endfm
==========================================
reduce in META-LEVEL : metaReduce(fmod 'FOO is
protecting 'BOOL .
sorts 'Foo .
none
op 'a : nil -> 'Foo [metadata("bla bla")] .
op 'b : nil -> 'Foo [metadata("bla bla")] .
none
eq 'a.Foo = 'b.Foo [metadata("hmm")] .
endfm, 'a.Foo) .
rewrites: 2
result ResultPair: {'b.Foo, 'Foo}
fmod BAR is
sorts Foo Bar .
subsort Foo < Bar .
op f : Foo -> Foo [metadata "fooy"] .
op f : Bar -> Bar [metadata "fubar"] .
endfm
fmod BAR is
sorts Foo Bar .
subsort Foo < Bar .
op f : Foo -> Foo [metadata "fooy"] .
op f : Bar -> Bar [metadata "fubar"] .
endfm
==========================================
reduce in META-LEVEL : upModule('BAR, false) .
rewrites: 1
result FModule: fmod 'BAR is
nil
sorts 'Bar ; 'Foo .
subsort 'Foo < 'Bar .
op 'f : 'Bar -> 'Bar [metadata("fubar")] .
op 'f : 'Foo -> 'Foo [metadata("fooy")] .
none
none
endfm
Bye.
|
