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
|
***
*** Test for the instantiation of a parameterized view containing an
*** op->term mapping by a module-view. Here the problem is in
*** the canonical renaming that is computed to map from the
*** parameterized view, PV{X :: T} from B to BASE{X} to its
*** instance, PV{MV} from B to BASE{MV}.
***
*** If the first user sort in a kind in BASE{X} does not appear
*** in the parameter theory copy of T then term->op mappings and
*** op->op mappings in this canonical renaming maybe missing this sort
*** and may fail to match. Then instantiating the op->term mapping will
*** cause a self-check failure.
***
*** The solution is to use BASE{X} to compute the sorts for the
*** operator mappings in the canonical renaming.
***
fth T is
sort Small .
op f : Small -> Small .
endfth
fmod M is
sort Num .
op s : Num -> Num .
endfm
view MV from T to M is
sort Small to Num .
op f to s .
endv
fth B is
sort Tiny .
op g : Tiny -> Tiny .
endfth
fmod USE-B{X :: B} is
eq g(N:X$Tiny) = N:X$Tiny [label "raw thumb"] .
endfm
fmod BASE{X :: T} is
sort Big .
subsort X$Small < Big . *** this triggers the bug
endfm
view PV{X :: T} from B to BASE{X} is
sort Tiny to X$Small .
op g(N:Tiny) to term f(f(N:X$Small)) .
endv
fmod TEST is
pr USE-B{PV{MV}} .
endfm
show eqs .
|
