0
|
1 /*
|
|
2
|
|
3 ?-com([upm,up]).
|
|
4 ?-tokio test.
|
|
5
|
|
6 Thu Sep 4 22:22:41 GMT+9:00 1986
|
|
7 */
|
|
8
|
|
9 :- static([
|
|
10 memory(_), g_addr, d_addr, g_cell, d_cell, g_mem, d_mem,
|
|
11 length, stack_ln(_), stack_ga(_), stack_da(_),
|
|
12 stack_depth, return_code, run, d_bus, g_bus]).
|
|
13
|
|
14
|
|
15 init:-
|
|
16 *length <= (*memory(*g_addr)..data - 1,int,0),
|
|
17 *d_addr <= (*d_addr..data + 2,int,*d_addr..map),
|
|
18 *g_addr <= (*g_addr..data + 2,int,*g_addr..map),
|
|
19 *stack_depth <= 0,
|
|
20 *run <= 1
|
|
21 && loop_unif.
|
|
22
|
|
23 loop_unif:-
|
|
24 if *length..data > 0
|
|
25 then fetch_unif1
|
|
26 else if *stack_depth = 0
|
|
27 then (*return_code <= (0,int,0), *run <= 0 && idle)
|
|
28 else *length <= *stack_ln(*stack_depth - 1),
|
|
29 *g_addr <= *stack_ga(*stack_depth - 1),
|
|
30 *d_addr <= *stack_da(*stack_depth - 1),
|
|
31 *stack_depth <= *stack_depth - 1
|
|
32 && fetch_unif1.
|
|
33
|
|
34 fetch_unif1:-
|
|
35 fetch_unif0g,
|
|
36 fetch_unif0d &&
|
|
37 *length <= (*length..data - 1,int,0),
|
|
38 *g_addr <= (*g_addr..data + 1,int, *g_addr..map),
|
|
39 *d_addr <= (*d_addr..data + 1,int, *d_addr..map) &&
|
|
40 fetch_unif2.
|
|
41
|
|
42 fetch_unif0g:-
|
|
43 fetch(*g_addr,*g_cell,*g_bus), *g_mem <= *g_addr &&
|
|
44 if *g_cell..tag = var
|
|
45 then fetch_unif1g.
|
|
46
|
|
47 fetch_unif1g:-
|
|
48 fetch(*g_cell,*g_cell,*g_bus), *g_mem <= *g_cell &&
|
|
49 if *g_cell..tag = var
|
|
50 then fetch_unif1g.
|
|
51
|
|
52 fetch_unif0d:-
|
|
53 fetch(*d_addr,*d_cell,*d_bus), *d_mem <= *d_addr &&
|
|
54 if *d_cell..tag = var
|
|
55 then fetch_unif1d.
|
|
56
|
|
57 fetch_unif1d:-
|
|
58 fetch(*d_cell,*d_cell,*d_bus), *d_mem <= *d_cell &&
|
|
59 if *d_cell..tag = var
|
|
60 then fetch_unif1d.
|
|
61
|
|
62 fetch_unif2:-
|
|
63 if *g_mem = *d_mem then loop_unif
|
|
64 else {
|
|
65 G = *g_cell..tag, D = *d_cell..tag, {
|
|
66 if (G=undef,D=undef) then
|
|
67 (store(*g_mem,*d_mem, *g_bus) && loop_unif)
|
|
68 else if (G=undef,D\=undef) then
|
|
69 (store(*g_mem,*d_cell,*g_bus) && loop_unif)
|
|
70 else if (G\=undef,D=undef) then
|
|
71 (store(*d_mem,*g_cell,*d_bus) && loop_unif)
|
|
72 else if (G=list,D=list) then
|
|
73 (if *length..data > 0
|
|
74 then ((*stack_depth <= *stack_depth + 1,
|
|
75 S<-- *stack_depth,
|
|
76 *stack_ga(S) <= *g_addr,
|
|
77 *stack_da(S) <= *d_addr,
|
|
78 *stack_ln(S) <= *length,
|
|
79 *length <= (2,int,g),
|
|
80 *g_addr <= *g_cell,
|
|
81 *d_addr <= *d_cell) && fetch_unif1)
|
|
82 else loop_unif)
|
|
83 else if (*g_cell..tag \= *d_cell..tag ;
|
|
84 *g_cell..data \= *d_cell..data) then
|
|
85 ((*return_code <= fail, *run <= 0) && idle)
|
|
86 else loop_unif }}.
|
|
87
|
|
88
|
|
89 idle:- if *run = 1
|
|
90 then (true && init).
|
|
91
|
|
92
|
|
93 test:-
|
|
94 *memory((0,_,g)) := (4,int,g), % length
|
|
95 *memory((1,_,g)) := (append,atom,g), % append
|
|
96 *memory((2,_,g)) := (100,list,g),
|
|
97 *memory((3,_,g)) := (200,list,g),
|
|
98 *memory((4,_,g)) := (300,var,g),
|
|
99 *memory((5,_,g)) := (2,int,g),
|
|
100 *memory((6,_,g)) := (print,atom,g), % print
|
|
101 *memory((7,_,g)) := (400,var,g),
|
|
102 *memory((8,_,g)) := (0,int,g), % length = 0
|
|
103 *memory((100,_,g)) := (a,atom,g),
|
|
104 *memory((101,_,g)) := (102,list,g),
|
|
105 *memory((102,_,g)) := (b,atom,g),
|
|
106 *memory((103,_,g)) := ([],atom,g),
|
|
107 *memory((200,_,g)) := (c,atom,g),
|
|
108 *memory((201,_,g)) := (102,list,g),
|
|
109 *memory((202,_,g)) := (d,atom,g),
|
|
110 *memory((203,_,g)) := ([],atom,g),
|
|
111 *memory((300,_,g)) := (0,undef,g),
|
|
112 *memory((400,_,g)) := (0,undef,g),
|
|
113 *memory((0,_,d)) := (5,int,d),
|
|
114 *memory((1,_,d)) := (append,atom,d), % append([H|X],Y,[H|Z])
|
|
115 *memory((2,_,d)) := (200,list,d),
|
|
116 *memory((3,_,d)) := (300,var,d),
|
|
117 *memory((4,_,d)) := (400,list,d),
|
|
118 *memory((5,_,d)) := (5,int,d),
|
|
119 *memory((6,_,d)) := (append,atom,d), % append([],X,X)
|
|
120 *memory((7,_,d)) := ([],atom,d),
|
|
121 *memory((8,_,d)) := (100,var,d),
|
|
122 *memory((9,_,d)) := (100,var,d),
|
|
123 *memory((100,_,d)) := (0,undef,d),
|
|
124 *memory((200,_,d)) := (500,var,d), % [H|X]
|
|
125 *memory((201,_,d)) := (600,var,d),
|
|
126 *memory((300,_,d)) := (0,undef,d), % Y
|
|
127 *memory((400,_,d)) := (700,list,d), % [H|Z]
|
|
128 *memory((500,_,d)) := (0,undef,d), % H
|
|
129 *memory((600,_,d)) := (0,undef,d), % X
|
|
130 *memory((700,_,d)) := (500,var,d), % H
|
|
131 *memory((701,_,d)) := (800,var,d), % Z
|
|
132 *memory((800,_,d)) := (0,undef,d), % Z
|
|
133 *g_addr := (0,int,g),
|
|
134 *d_addr := (0,int,d),
|
|
135 *return_code := (0,undef,0),
|
|
136 *length := (0,int,0),
|
|
137 *g_mem := (0,int,g),
|
|
138 *d_mem := (0,int,d),
|
|
139 *g_cell := (0,int,g),
|
|
140 *d_cell := (0,int,d),
|
|
141 *run := 0,
|
|
142 *d_bus := free, *g_bus := free,
|
|
143 *stack_depth := 0 &&
|
|
144 init,
|
|
145 # (Write = (*g_addr, *d_addr, *return_code, *run, *length,
|
|
146 *g_mem, *d_mem, *g_cell, *d_cell, *stack_depth,
|
|
147 *g_bus, *d_bus), write(Write) ).
|