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
|
***
*** Counterpart of the viewInstantiationByModuleViewApril2025 test for
*** strategy to strategy expression mappings.
***
sth T is
sort Small .
strat f : Small @ Small .
endsth
smod M is
sort Num .
strat s : Num @ Num .
endsm
view MV from T to M is
sort Small to Num .
strat f to s .
endv
sth B is
sort Tiny .
strat g : Tiny @ Tiny .
endsth
smod USE-B{X :: B} is
sd g(N:X$Tiny) := match N:X$Tiny [label "raw thumb"] .
endsm
smod BASE{X :: T} is
sort Big .
subsort X$Small < Big . *** this triggers the bug
endsm
view PV{X :: T} from B to BASE{X} is
sort Tiny to X$Small .
strat g(N:Tiny) to expr f(N:X$Small) .
endv
smod TEST is
pr USE-B{PV{MV}} .
endsm
show sds .
|
