-
Notifications
You must be signed in to change notification settings - Fork 12
/
Copy pathtemplate.src
2758 lines (2398 loc) · 101 KB
/
template.src
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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
% $Date: 91/09/10 14:48:43 $
% $Revision: 1.9 $
% (c) 1991 Simon Peyton Jones & David Lester.
H> module Template where
H> import Language
H> import Utils
\chapter{Template instantiation}
\label{sect:template}
This chapter introduces the simplest possible implementation of
a functional language: a graph reducer based
on \stressD{template instantiation}.
The complete source code for an initial version (Mark 1) is given, followed
by a series of improvements and variations on the basic design.
We begin with a review of graph reduction and template instantiation.
\section{A review of template instantiation}
We begin with a brief overview of template instantiation.
This material is covered in more detail in
Chapters 11 and 12 of \cite{PJBook}.
We recall the following key facts:
\begin{itemize}
\item
A functional program is `executed' by {\em evaluating an expression}.
\item
The expression is represented by a {\em graph}\indexD{graph}.
\item
Evaluation takes place by carrying out a sequence of
\stressD{reductions}.
\item
A reduction replaces (or {\em updates\/}\index{updates})
a \stressD{reducible expression}
in the graph
by its reduced form. The term `reducible expression' is often
abbreviated to `redex'\index{redex}.
\item
Evaluation is complete when there are no more redexes; we say that the
expression is in \stressD{normal form}.
\item
At any time there may be more than one redex in the expression being
evaluated, so there is a choice about which one to reduce next.
Fortunately, whatever reduction sequence we choose, we will always get the
same answer (that is, normal form). There is one caveat: some reduction
sequences may fail to terminate.
\index{termination}
\item
However, if
any choice of redexes makes evaluation terminate, then the policy of
always selecting the outermost redex will also do so.
This choice of reduction order is called
\stressD{normal order reduction}, and it is the one we will always use.
\end{itemize}
\begin{together}
Thus the process of evaluation can be described as follows:
\begin{verbatim}
until there are no more redexes
select the outermost redex
reduce it
update the (root of the) redex with the result
end
\end{verbatim}
\end{together}
\subsection{An example}
As an example, consider the following Core-language program:
\begin{verbatim}
square x = x * x ;
main = square (square 3)
\end{verbatim}
The program consists of a set of definitions, called {\em supercombinators\/};
@square@ and @main@ are both supercombinators\indexD{supercombinator}.
By convention, the expression to be evaluated is the supercombinator @main@.
Hence, to begin with the expression to be evaluated is represented by the
following rather trivial tree
(remember that a tree is just a special sort of graph):
\begin{verbatim}
main
\end{verbatim}
Now, since @main@ has no arguments, it itself is a redex, so we replace it
by its body:
\begin{verbatim}
main reduces to @
/ \
square @
/ \
square 3
\end{verbatim}
Applications are represented by {\tt @@} signs in these pictures and all
subsequent ones.
Now the outermost redex is the outer application of @square@.
To reduce a function application we replace the redex with
an instance of the body of the function, substituting a pointer to the
argument for each occurrence of the formal parameter, thus:
\begin{verbatim}
@! reduces to @!
/ \ / \
square @ @ \
/ \ / \___@
square 3 * / \
square 3
\end{verbatim}
The root of the redex, which is overwritten with the result, is marked with
a @!@.
Notice that the inner @square 3@ redex has become shared, so that
the tree has become a graph.
In the definition of @square@ the expression @x*x@ (in which the @*@ is
written infix) is just short for @((* x) x)@, the application of @*@ to
two arguments. We use {\em currying\/} to write functions of several
arguments in terms of one-argument applications: @*@ is a function
which, when applied to an argument @p@, gives a function which, when
applied to another argument @q@, returns the product of @p@ and @q@.
Now the only redex is the inner application of @square@ to @3@. The
application of @*@ is not reducible because @*@ requires its arguments to
be evaluated.
The inner application is reduced like this:
\begin{verbatim}
@ reduces to @
/ \ / \
@ \ @ \
/ \___@! / \___@
* / \ * / \
square 3 @ \
/ \___3
*
\end{verbatim}
There is still only one redex, the inner multiplication. We replace
the redex with the result of the multiplication, @9@:
\begin{verbatim}
@ reduces to @
/ \ / \
@ \ @ \
/ \___@! / \___9
* / \ *
@ \
/ \___3
*
\end{verbatim}
Notice that by physically updating the root of the redex with the
result, both arguments of the outer multiplication `see' the result
of the inner multiplication.
The final reduction is simple:
\begin{verbatim}
@ reduces to 81
/ \
@ \
/ \___9
*
\end{verbatim}
\subsection{The three steps}
As we saw earlier, graph reduction consists of repeating the following
three steps until a normal form is reached:
\begin{enumerate}
\item
Find the next redex.
\item
Reduce it.
\item
Update the (root of the) redex with the result.
\end{enumerate}
As can be seen from the example in the previous section,
there are two sorts of redex, which are
reduced in different ways:
\begin{description}
\item[Supercombinators.]
If the outermost function application is a supercombinator application,
then it is certainly also a redex, and it can be reduced as described
below (Section~\ref{sect:templ:supercomb-review}).
\item[Built-in primitives.]
If the outermost function application is the application of a built-in
primitive\index{primitives}%
, then the application may or may not be a redex, depending on
whether the arguments are evaluated.
If not, then the arguments must be evaluated.
This is done using exactly the same process: repeatedly find the outermost
redex of the argument and reduce it.
Once this is done, we can return to the reduction of the outer application.
\end{description}
\subsection{Unwinding the spine to find the next redex}
The first step of the reduction cycle is to find the site of the next
reduction to be performed;
that is, the outermost reducible function application.
It is easy to find the outermost function application (though it may
not be reducible) as follows:
\begin{enumerate}
\item
Follow the
left branch of the application nodes, starting at the root, until you
get to a supercombinator or built-in primitive.
This left-branching chain of application nodes is called the {\em spine\/}
of the expression, and this process is called {\em unwinding\/}\index{unwind}
the spine.
Typically a {\em stack\/}\index{stack} is used to remember
the addresses of the nodes encountered on the way down.
\item
Now, check how many arguments the supercombinator or primitive
takes and go back up
that number of application nodes; you have now found the root of the
outermost function application.
\end{enumerate}
For example, in the expression @(f E1 E2 E3)@, where @f@ takes two arguments,
say, the outermost function application is @(f E1 E2)@. The expression and
stack would look like this:
\begin{verbatim}
Stack
-----------
| ---|-------> @
------- / \
| ---|-----> @! E3
------- / \
| ---|---> @ E2
------- / \
| ---|-> f E1
-------
\end{verbatim}
The (root of the) outermost function application is marked with a @!@.
If the result of an evaluation could be a partial
application\index{partial applications}, as would be the case if @f@ took
four arguments instead of two, then step 2 above needs to be preceded
by a check there are enough application nodes in the spine. If not,
the expression has reached {\em weak head normal form\/} (WHNF).
\indexD{weak head normal form}
The
sub-expressions @E1@, @E2@ and @E3@ might still contain redexes, but
most evaluators will stop when they reach WHNF rather than trying to
reduce the sub-expressions also. If the program has been type-checked,
and the result is guaranteed to be a number, say, or a list, then this
underflow check\index{stack underflow check}
can be omitted.
Notice that we have only found the root of the outermost {\em function
application}. It may or may not be a {\em redex\/} as well. If the function
is a supercombinator, then it will certainly be a redex, but if it is
a primitive, such as @+@, then it depends on whether its arguments are
evaluated. If they are, we have found the outermost redex. If not, we have
more work to do.
If a primitive\index{primitives}
requires the value of a currently unevaluated argument,
we must
evaluate the argument before the primitive reduction can proceed.
To do this, we must put the current stack on one
side, and begin with a new stack to reduce the argument, in the same
way as before. This was the situation in the example of the previous section
when we reached the stage
\begin{verbatim}
@
/ \
@ \
/ \___@
* / \
square 3
\end{verbatim}
We need to evaluate the argument @(square 3)@ on a new
stack. During this evaluation, we might again encounter a primitive
with an unevaluated argument, so we would need to start a new evaluation
again. We need to keep track of all the `old' stacks, so that we come
back to them in the right order. This is conveniently done by keeping
a stack of stacks, called the {\em dump}. When we need to evaluate an
argument, we push the current stack onto the dump\index{dump}%
; when we have finished
an evaluation we pop the old stack off the dump.
Of course, in a real implementation we would not copy whole stacks!
Since the `new' stack will be finished with before the `old' one is again
required, the `new' one could be built
physically on top of the `old' one.
The dump stack would then just keep track of where the boundary between
`new' and `old' was. Conceptually, though, the dump is a stack of stacks,
and we will model it in this way.
\subsection{Supercombinator redexes}
\label{sect:templ:supercomb-review}
A supercombinator redex is reduced by substituting the arguments into
its body. More precisely:
\begin{important}
{\em Supercombinator reduction}. A supercombinator redex is reduced
by replacing the
redex with an instance of the
supercombinator body, substituting pointers to the actual arguments for
corresponding occurrences of the formal parameters.
Notice that the arguments are
not copied; rather, by the device of using pointers
to them, they are shared.\index{instantiation}
\end{important}
A supercombinator body may contain @let@ and @letrec@ expressions.
For example:
\begin{verbatim}
f x = let y = x*x
in y+y
\end{verbatim}
@let@ and @letrec@ expressions are treated as {\em textual descriptions of
a graph}. Here, for example, is a possible use of the definition of @f@:
\begin{verbatim}
@ reduces to @
/ \ / \
f 3 @ \
/ \___@y
+ / \
@ \
/ \___3
*
\end{verbatim}
The @let@ expression defines a sub-expression @x*x@, which is named @y@.
The body of the @let@ expression, @y+y@, uses pointers to the sub-expression
in place of @y@. Thus ordinary expressions describe trees; @let@ expressions
describe acyclic graphs; and @letrec@ expressions describe cyclic
graphs.
\subsection{Updates}
\label{sect:templ:update-review}
After performing a reduction, we must update the root of the redex with
the result, so that if the redex is shared (as it was in the example
@(square (square 3))@) the reduction is only done once.
This updating is the essence of {\em lazy
evaluation}.
A redex may not be evaluated at all but, if it is evaluated, the
update ensures that the cost of doing so is incurred at most once.
\index{updates}
Omitting the updates does not cause any errors; it will just mean that
some expressions may be evaluated more than once, which is inefficient.
There is one case that requires a little care when performing updates.
Consider the program
\begin{verbatim}
id x = x
f p = (id p) * p
main = f (sqrt 4)
\end{verbatim}
After the @f@ reduction has taken place, the graph looks like this:
\begin{verbatim}
@
/ \
@ \
/ \ \
* @ \
/ \___@
id / \
sqrt 4
\end{verbatim}
We assume @sqrt@ is a built-in primitive for taking square roots.
Now, suppose that the next redex selected is the first argument of the @*@,
namely the application of @id@.
(It might equally well be the second argument of @*@, since neither argument
is in normal form, but we will suppose it is the first.)
What should we overwrite the root of the redex with after performing the
@id@ reduction? {\em We should certainly not overwrite it with a
copy of the @(sqrt 4)@ application node,
because then @(sqrt 4)@ would be evaluated twice!}
The easiest way out of this dilemma is to add a new sort of graph node,
an {\em indirection node}\index{indirections},
which will be depicted as a @#@ sign. An
indirection node can be used to update the root of a redex to point to
the result of the reduction:
\begin{verbatim}
@ reduces to @
/ \ / \
@ \ @ \
/ \ \ / \ \
* @ \ * # \
/ \___@ \___@
id / \ / \
sqrt 4 sqrt 4
\end{verbatim}
Section 12.4 of \cite{PJBook} contains further discussion of the
issues involved in updates.
\subsection{Constant applicative forms\advanced}
\label{sect:caf}
Some supercombinators have no arguments; they are called {\em constant
applicative forms}, or CAFs.
\index{CAF}
For example, @fac20@ is a CAF:
\begin{verbatim}
fac20 = factorial 20
\end{verbatim}
The interesting thing about CAFs is that {\em the supercombinator itself
is a redex}. We do not want to instantiate a new copy of @factorial 20@
whenever @fac20@ is called, because that would mean repeating the
computation of @factorial 20@. Rather, the supercombinator @fac20@ is
the root of the @fac20@-reduction, and should be overwritten with the
result of instantiating its body.
The practical consequence is that supercombinators should be represented
by graph nodes, in order that they can be updated in the usual way.
We will see this happening in practice in each of our implementations.
This concludes our review of graph reduction.
\section{State transition systems}
We now turn our attention to implementing graph reduction.
We will describe each of our implementations using a
{\em state transition system}.
In this section we introduce state transition systems.
A state transition system
\index{state transition system} is a notation for describing the
behaviour of a sequential machine.
At any time, the machine is in some {\em state}, beginning with a specified
{\em initial state}.
If the machine's state {\em matches\/} one of the
{\em state transition rules}, the rule {\em fires\/} and specifies a
new state for the machine.
When no state transition rule matches, execution halts.
If more than one rule matches, then one is chosen arbitrarily to fire; the
machine is then {\em non-deterministic}. All our machines will be
deterministic.
Here is a simple example of a state transition system used to
specify a (rather inefficient) multiplication machine. The state is a
quadruple $(n,m,d,t)$. The numbers to be multiplied are $n$ and $m$, and
the running total is $t$, and
the machine is initialised to the state $(n,m,0,0)$.
The operation of the machine is specified by two transition rules.
The $d$ component is
repeatedly decremented towards zero while simultaneously incrementing $t$,
as specified by the first rule:
\begin{flushleft}
\qquad $\begin{array}{|lllll|}
\hline
& n & m & d & t \\
\Longrightarrow & n & m & d-1 & t+1 \\
& \multicolumn{4}{l|}{\mbox{where}~d>0} \\
\hline
\end{array}$
\end{flushleft}
We always write transition rules with each component of the new state
directly underneath the same component of the old state, so that it is
easy to see which components have changed.
When $d$ reaches zero it is initialised again to $n$, and $m$ is decremented,
until $m$ reaches zero. This is specified by the second rule:
\begin{flushleft}
\qquad $\begin{array}{|lllll|}
\hline
& n & m & 0 & t \\
\Longrightarrow & n & m-1 & n & t \\
& \multicolumn{4}{l|}{\mbox{where}~m>0} \\
\hline
\end{array}$
\end{flushleft}
The machine terminates when no rule applies. At this point it will be
in a state $(n,0,0,t)$, where $t$ is the product of $n$ and $m$ from the
initial state.
\begin{exercise}
Run the machine by hand
starting with initial state $(2,3,0,0)$, specifying
which rule fires at each step. Verify that the final state is $(2,0,0,6)$.
\end{exercise}
\begin{exercise}
An invariant\index{invariant} of a sequence of states is a predicate
which is true of all of the states. Find an invariant which expresses
the relationship between the initial value of $n$ and $m$ (call them
$N$ and $M$), and the current values of $m$, $d$ and $t$. Hence {\em
prove\/} the conjecture that the machine performs multiplication. To do
the proof you need to show that
\begin{enumerate}
\item
The invariant is true for the initial state.
\item
If the invariant is true for a particular state, then it is
true for its successor state.
\item
Given the invariant and the termination condition ($m=d=0$),
then $t = N*M$.
\item
The machine terminates.
\end{enumerate}
\end{exercise}
State transition systems are convenient for our purposes, because:
\begin{itemize}
\item
They are sufficiently {\em abstract\/} that we do not get tangled up in very
low-level details.
\item
They are sufficiently {\em concrete\/} that we can be sure we are
not `cheating' by hiding a lot of complexity in the rules.
\item
We can transliterate a state transition system directly into Miranda
to give an executable implementation of the system.
\end{itemize}
To illustrate the last point, we will transliterate the multiplication
machine into Miranda. We begin by giving a type synonym to define the
type of a state in this machine:
M1> multState == (num, num, num, num) || (n, m, d, t)
GH1> type MultState = (Int, Int, Int, Int) -- (n, m, d, t)
Next, the function @evalMult@ takes a state and
returns the list consisting of that state followed by all
the states which follow it:
M1> evalMult :: multState -> [multState]
M1> evalMult state = [state], multFinal state
M1> = state : evalMult (stepMult state), otherwise
GH1> evalMult :: MultState -> [MultState]
GH1> evalMult state = if multFinal state
GH1> then [state]
GH1> else state : evalMult (stepMult state)
The function @stepMult@ takes a non-final state and returns the next state.
There is one equation for @stepMult@ for each transition rule:
M1> stepMult (n, m, d, t) = (n, m, d-1, t+1), d>0
M1> stepMult (n, m, d, t) = (n, m-1, n, t), d=0
GH1> stepMult (n, m, d, t) | d > 0 = (n, m, d-1, t+1)
GH1> stepMult (n, m, d, t) | d == 0 = (n, m-1, n, t)
The function @multFinal@ takes a state and
tests whether the state is a final state:
M1> multFinal :: multState -> bool
GH1> multFinal :: MultState -> Bool
\begin{exercise}
Define the function @multFinal@, and run the resulting machine on
the initial state $(2,3,0,0)$, checking that the last state of the result
list is $(2,0,0,6)$. You may find the standard function @layn@ is useful
to help lay out the results more legibly.
\end{exercise}
\section{Mark 1: A minimal template instantiation graph reducer}
\index{template instantiation machine!Mark 1}
We are now ready to begin the definition of a rather simple graph reducer.
Even though it is simple, it contains many of the parts
that more sophisticated graph reducers have, so it takes a few pages
to explain.
\subsection{Transition rules for graph reduction}
\label{sect:templ:transition-rules}
The state of the template instantiation graph reduction machine
is a quadruple
\[
\mbox{\em (stack, dump, heap, globals)}
\]
or {\em(s,d,h,f)\/} for short.
\begin{itemize}
\item
The {\em stack\/} is a stack of {\em addresses}, each of which
identifies a {\em node\/} in the heap.
These nodes form the spine of the expression being
evaluated.
The notation $a_1:s$ denotes a stack whose top
element is $a_1$ and the rest of which is $s$.
\item
The {\em dump\/}\index{dump} records the state of the spine stack
\index{spine stack}
prior to
the evaluation of an argument of a strict primitive.
The dump will not be used at all in the Mark 1 machine, but it will
be useful for subsequent versions.
\item
The {\em heap\/}\index{heap} is a collection of tagged {\em nodes}\index{node}.
The notation $h[a:node]$ means that
in the heap $h$
the address $a$ refers to the node $node$.
\item
For each supercombinator (and later for each primitive),
{\em globals\/}\index{global}
gives the address of heap node representing the supercombinator
(or primitive).
\end{itemize}
A heap node can take one of three forms (for our most primitive machine):
\begin{itemize}
\item
$@NAp@~a_1~a_2$ represents
the application of the node whose address is $a_1$ to that
whose address is $a_2$.
\item
$@NSupercomb@~args~body$ represents a supercombinator
with arguments $args$ and body $body$.
\item
$@NNum@~n$ represents the number $n$.
\end{itemize}
There are only two state transition rules for this primitive
template instantiation machine. The first one describes how to
unwind\index{unwind}
a single application node onto the spine stack:
\tirule{
\tistate{a:s}{d}{h[a:@NAp@~ a_1~ a_2]}{f}
}{
\tistate{a_1:a:s}{d}{h}{f}
}
\label{rule:unwind}
(The heap component of the second line of this rule still includes the
mapping of address $a$ to $@NAp@~a_1~a_2$, but we do not write it out
again, to save clutter.)
Repeated application of this rule will unwind the entire spine of
the expression onto the stack, until the node on top of the stack
is no longer a @NAp@ node.
The second rule describes how to perform a
supercombinator reduction.\index{supercombinator!reduction}
\tirulew{
\tistate{a_0:a_1:\ldots:a_n:s}{d}
{h[a_0:@NSupercomb@~ [x_1,\ldots,x_n]~body]}
{f}
}{
\tistate{a_r:s}{d}{h'}{f}
}{
(h',a_r) = instantiate~ body~ h~
f[x_1 \mapsto a_1,~ \ldots,~ x_n \mapsto a_n]
}
\label{rule:sc1}
Most of the interest in this rule is hidden inside the
function $instantiate$. Its arguments are:
\begin{itemize}
\item
the expression to instantiate,
\item
a heap,
\item
the global mapping of names to heap addresses, $f$, augmented
by the mapping of argument names to their addresses obtained from the
stack.
\end{itemize}
It returns a new heap and the address of the (root of the) newly constructed
instance.
Such a powerful operation is
really at variance with the spirit of state transition systems,
where each step is meant to be a simple atomic action, but that is the
nature of the template instantiation machine.
The implementations of later chapters will all have truly atomic actions!
Notice that the root of the redex is not itself affected by this rule;
it is merely replaced on the stack by the root of the result.
In other words, these rules describe a tree-reduction machine,
which does {\em not\/} update\index{updates}
the root of the redex, rather
than a graph-reduction
machine.
We will improve on this later in Section \ref{sect:templ:update}.
\subsection{Structure of the implementation}
Now that we have a specification of our machine, we are ready
to embark on its implementation.
Since we are writing the implementation in a functional language,
we must write a function @run@, say,
to do the job. What should its type be?
It should take a filename, run the program therein, and print
out the results, which might be either the final result or some kind
of execution trace.
So the type of @run@ is given by the following type signature:
M> run :: [char] -> [char]
GH> runProg :: [Char] -> [Char] -- name changed to not conflict
\par
Now we can think about how @run@ might be built up. Running a program
consists of four stages:
\begin{enumerate}
\item
Parse the program from the expression found in a specified file.
The @parse@ function takes a filename and returns the parsed program.
M0> parse :: [char] -> coreProgram
GH0> parse :: [Char] -> CoreProgram
\item
Translate the program
into a form suitable for execution. The @compile@ function,
which performs this task, takes a program and
produces the initial state of the template instantiation machine:
M> compile :: coreProgram -> tiState
GH> compile :: CoreProgram -> TiState
@tiState@ is the type of the state of the template instantiation machine.
(The prefix `@ti@' is short for template instantiation.)
\item
Execute the program, by performing repeated state transitions until
a final state is reached. The result is a list of all the states passed
through; from this we can subsequently
either extract the final state, or get a trace
of all the states.
For the present we will restrict ourselves to programs which return
a number as their result, so we call this execution function @eval@.
M> eval :: tiState -> [tiState]
GH> eval :: TiState -> [TiState]
\item
Format the results for printing. This is done by the function @showResults@,
which selects which information to print, and formats it into a
list of characters.
M> showResults :: [tiState] -> [char]
GH> showResults :: [TiState] -> [Char]
\end{enumerate}
The function @run@ is just the composition of these four functions:
M> run = showResults . eval . compile . parse
GH> runProg = showResults . eval . compile . parse -- "run": name conflict
We will devote a subsection to each of these phases.
\subsection{The parser}
The source language, including the @parse@ function,
is defined in a separate module @language@, defined
in Chapter~\ref{sect:language}.
We make it available using the
@%include@ directive to import the module:
M> %include "language"
G> -- :a language.lhs
H> -- import Language
\subsection{The compiler}
In this section we define the @compile@ function. We will need
the data types and functions defined in the @utils@ module, so we
use @%include@ to make it available.
M> %include "utils"
G> -- :a utils.lhs
H> -- import Utils
Now we need to consider the representation of the data types the
compiler manipulates.
\subsubsection{Data types}
The compiler produces the initial state of the machine, which has
type @tiState@, so the next thing to do is to define how machine states
are represented, using a type synonym\index{type synonym}:
M> tiState == (tiStack, tiDump, tiHeap, tiGlobals, tiStats)
GH> type TiState = (TiStack, TiDump, TiHeap, TiGlobals, TiStats)
The state of the machine is a quintuple whose first four components correspond
exactly to those given in Section~\ref{sect:templ:transition-rules}, and whose
fifth component is used to accumulate statistics.
Next, we need to consider the representation of each of these components.
\begin{itemize}
\item
The {\em spine stack\/}\index{spine stack}
is just a stack of {\em heap addresses\/}:
M> tiStack == [addr]
GH> type TiStack = [Addr]
We choose to represent the stack as a list. The elements of the stack
are members of the abstract data type @addr@ defined in the @utils@
module (Appendix~\ref{sect:heap}).
They represent heap addresses, and by making them abstract we ensure that
we can only use the operations provided on them by the @utils@ module.
Thus it is impossible for us to add one to an address, say, by mistake.
\item
The {\em dump\/} is
not required until Section~\ref{sect:templ:primitives}, but we make it
part of the state already because adding it later would require many tiresome
alterations to the state transition rules. For now we give it a trivial
type definition, consisting of just a single constructor with no arguments.
M1-3> tiDump ::= DummyTiDump
GH1-3> data TiDump = DummyTiDump
1-3> initialTiDump = DummyTiDump
\item
The {\em heap\/} is represented by the @heap@ abstract data type defined in
the @utils@ module. We have to say what the heap contains, namely objects
of type @node@ (yet to be defined):
M> tiHeap == heap node
GH> type TiHeap = Heap Node
Heap @node@s are represented by the following algebraic data type
declaration, which corresponds to the list of possibilities given in
Section~\ref{sect:templ:transition-rules}:
M1-2> node ::= NAp addr addr || Application
M1-2> | NSupercomb name [name] coreExpr || Supercombinator
M1-2> | NNum num || A number
GH1-2> data Node = NAp Addr Addr -- Application
GH1-2> | NSupercomb Name [Name] CoreExpr -- Supercombinator
GH1-2> | NNum Int -- A number
The only difference is that we have added an extra field of type
@name@ to the @NSupercomb@ constructor, which is used to hold the name
of the supercombinator. This is used only for documentation and
debugging purposes.
\item
The {\em globals\/} component associates each
supercombinator name with
the address of a heap node containing its definition:
M> tiGlobals == assoc name addr
GH> type TiGlobals = ASSOC Name Addr
The @assoc@ type is defined in the @utils@ module, along with its
operations (Appendix~\ref{sect:assoc}).
It is actually defined there as a type synonym (not an abstract
data type) because it is so convenient to be able to manipulate associations
using the built-in syntax for lists. There is a tension here between
abstraction and ease of programming.
\item
The @tiStats@ component of the state is not mentioned in the
transition rules, but we will use it to collect run-time performance
statistics\index{statistics} on what the machine does.
So that we can easily change what statistics are collected,
we will make it an abstract type. To begin with, we will record only
the number of steps taken:
M> abstype tiStats
M> with tiStatInitial :: tiStats
M> tiStatIncSteps :: tiStats -> tiStats
M> tiStatGetSteps :: tiStats -> num
GH> tiStatInitial :: TiStats
GH> tiStatIncSteps :: TiStats -> TiStats
GH> tiStatGetSteps :: TiStats -> Int
The implementation is rather simple:
M> tiStats == num
GH> type TiStats = Int
> tiStatInitial = 0
> tiStatIncSteps s = s+1
> tiStatGetSteps s = s
A useful function @applyToStats@ applies a given function to the
statistics\index{statistics}
component of the state:
M> applyToStats :: (tiStats -> tiStats) -> tiState -> tiState
GH> applyToStats :: (TiStats -> TiStats) -> TiState -> TiState
> applyToStats stats_fun (stack, dump, heap, sc_defs, stats)
> = (stack, dump, heap, sc_defs, stats_fun stats)
\end{itemize}
This completes our definition of the data types involved.
\subsubsection{The compiler itself}
\label{sect:ti:compiler}
\label{sect:mapAccuml-example}
The business of the compiler is to take a program, and from
it create the initial state of the machine:
> compile program
> = (initial_stack, initialTiDump, initial_heap, globals, tiStatInitial)
> where
> sc_defs = program ++ preludeDefs ++ extraPreludeDefs
>
> (initial_heap, globals) = buildInitialHeap sc_defs
>
> initial_stack = [address_of_main]
> address_of_main = aLookup globals "main" (error "main is not defined")
\par
Let us consider each of the definitions in the @where@ clause in turn.
The first, @sc_defs@, is just a list
of all the supercombinator definitions involved in the program.
Recall that @preludeDefs@ was defined in Section~\ref{sect:prelude}
to be the list of standard supercombinator definitions which
are always included in every program. @extraPreludeDefs@ is a list of
any further standard functions we may want to add; for the present it is
empty:
1-4> extraPreludeDefs = []
\par
The second definition uses an auxiliary function, @buildInitialHeap@, to
construct an initial heap containing an @NSupercomb@ node for
each supercombinator, together with an association list @globals@ which
maps each supercombinator name onto the address of its node.
Lastly, @initial_stack@ is defined to contain just one item, the address
of the node for the supercombinator @main@, obtained from @globals@.
Now we need to consider the definition of @buildInitialHeap@,
which is a little
tricky. We need to do something for each element of the list @sc_defs@,
but what makes it awkward is that the `something' involves heap allocation.
Since each heap allocation produces a new heap, we need to find a way of
passing the heap along from one element of @sc_defs@ to the next.
This process starts with the empty heap, @hInitial@
(Appendix~\ref{sect:heap}).
We encapsulate this idea in a higher-order function\index{higher-order function}
@mapAccuml@, which
we will use quite a lot in this book. @mapAccuml@ takes three
arguments: $f$, the `processing function'; $acc$, the
`accumulator'; and a list $[x_1, \ldots, x_n]$. It takes each
element of the input list, and applies $f$ to it and the current
accumulator\index{accumulator}. $f$ returns a pair of results, an
element of the result list and a new value for the accumulator.
@mapAccuml@ passes the accumulator along from one call of $f$ to the
next, and eventually returns a pair of results: $acc'$, the final
value of the accumulator; and the result list $[y_1, \ldots, y_n]$.
Figure~\ref{fig:mapAccuml} illustrates this plumbing. The definition
of @mapAccuml@ is given in Appendix~\ref{sect:util-funs}.
\begin{figure} %\centering
\input{map_acc.tex}
\caption{A picture of $@mapAccuml@~f~acc~[x_1,\ldots,x_n]$}
\label{fig:mapAccuml}
\end{figure}
In our case, the `accumulator' is the heap, with initial value
@hInitial@. The list $[x_1,\ldots,x_n]$ is the supercombinator
definitions, @sc_defs@, while the result list $[y_1, \ldots, y_n]$ is
the association of supercombinator names and addresses, @sc_addrs@.
Here, then, is the definition of @buildInitialHeap@.
M1-3> buildInitialHeap :: [coreScDefn] -> (tiHeap, tiGlobals)
GH1-3> buildInitialHeap :: [CoreScDefn] -> (TiHeap, TiGlobals)
1-3> buildInitialHeap sc_defs = mapAccuml allocateSc hInitial sc_defs
\par
The `processing function', which we will call @allocateSC@,
allocates a single supercombinator, returning a new heap and a member
of the @sc_addrs@ association list.
M> allocateSc :: tiHeap -> coreScDefn -> (tiHeap, (name, addr))
GH> allocateSc :: TiHeap -> CoreScDefn -> (TiHeap, (Name, Addr))
> allocateSc heap (name, args, body)
> = (heap', (name, addr))
> where
> (heap', addr) = hAlloc heap (NSupercomb name args body)
That completes the definition of the compiler. Next, we turn our attention
to the evaluator.
\subsection{The evaluator\index{evaluator}}
The evaluator @eval@ takes an initial machine state,
and runs the machine one step at a time, returning the list of
all states it has been through.
@eval@ always returns the current state as the first element of its
result. If the current state is a final state, no further states are
returned; otherwise, @eval@ is applied recursively to the next state.
The latter is obtained by
taking a single step (using @step@), and then calling @doAdmin@ to
do any administrative work required between steps.
> eval state = state : rest_states
> where
M> rest_states = [], tiFinal state
M> = eval next_state, otherwise
GH> rest_states | tiFinal state = []
GH> | otherwise = eval next_state
> next_state = doAdmin (step state)
M> doAdmin :: tiState -> tiState
GH> doAdmin :: TiState -> TiState
> doAdmin state = applyToStats tiStatIncSteps state
\subsubsection{Testing for a final state}
The function @tiFinal@ detects the final state\index{final state}.
We are only finished if the stack contains a single object, and it is
either a number or a data object.
M1-3> tiFinal :: tiState -> bool
GH1-3> tiFinal :: TiState -> Bool
1-3>
1-3> tiFinal ([sole_addr], dump, heap, globals, stats)
1-3> = isDataNode (hLookup heap sole_addr)