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
|
*** Colliding Deterministic Reduction Paths for Leo's algorithm
set print mixfix off .
fmod COLLIDING-DRPs is
sorts A B C D .
op a_ : B -> A .
op b_ : C -> B .
op c_ : D -> C .
op d e : -> D .
op c d e : -> C .
endfm
*** ambiguous
parse a b c d e .
fmod COLLIDING-DRPs2 is
sorts A B C D .
op a_ : B -> A .
op b_ : C -> B .
op c d e : -> C .
op c _ e : D -> C .
op d : -> D .
endfm
*** ambiguous
parse a b c d e .
fmod SUB-DRP is
sorts A B C D E F G .
op a_ : B -> A [prec 10 gather (E)] .
op b_ : C -> B [prec 10 gather (E)] .
op c_ : D -> C [prec 10 gather (E)] . *** t2
op d e : -> D [prec 10] . *** t1
op _e : E -> D [prec 1 gather (E)] . *** r2
op d : -> E .
op __ : G D -> F [prec 1 gather (E E)] . *** u2
op c : -> G .
op a b_ : F -> A [prec 10 gather (E)] .
endfm
*** ambiguous - need to avoid generating the same parse twice
parse a b c d e .
fmod SUB-DRP2 is
sorts A B C D E F G H .
op a_ : B -> A [prec 10 gather (E)] .
op b_ : C -> B [prec 10 gather (E)] .
op c_ : D -> C [prec 10 gather (E)] . *** t2
op d_ : H -> D [prec 10] . *** now above t1
op e : -> H . *** new t1
op _e : E -> D [prec 1 gather (E)] . *** r2
op d : -> E .
op __ : G D -> F [prec 1 gather (E E)] . *** u2
op c : -> G .
op a b_ : F -> A [prec 10 gather (E)] .
endfm
*** ambiguous - need to avoid generating the same parse twice
parse a b c d e .
|
