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
|
+++
title = "Bluespec"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["1d"]
forwardlinks = ["1b2", "3a", "1b1"]
zettelid = "1d1"
+++
Bluespec is a higher-level hardware description language, based on
circuit generation instead of circuit description.
{{< transclude-1 zettel="1b2" >}}
Tail calls are an optimisation that can be applied in software, which
detects that a recursive call only happens at the tail of the function.
If that is the case, then the recursive call can happen without having
to preserve the stack at every call, as it can effectively be translated
to an equivalent version that only uses loops. This optimisation is
important to improve the efficiency of recursive functions if the stack
is not needed, and is especially important in functional languages where
recursion might be more widely used.
As tail calls can be efficiently translated to loops, this also means
that they can be efficiently encoded in hardware when the code is passed
through high-level synthesis. This is straightforward if the tail calls
are detected and automatically translated to loops, however, what
happens if that is not the case and we only have a tail call construct
in the intermediate language.
The CompCert ([\#3a]) \[1\] register transfer language (RTL)
intermediate language, for example, has an explicit tail call construct
(`Itailcall`), which is used if it can detect that a function contains a
tail call. Apart from that, it only has a jump command, which can be
used for loops. Therefore, supporting the tail call construct allows us
to support a subset of possible recursive functions. Even though these
are as powerful as loops, it may be more natural to write their
definitions as a recursive function instead of a loop.
{{< transclude-2 zettel="1b1" >}}
Guarded commands \[2\] are an interesting construct which can be added
to languages. They look similar to `case` statements, but behave in a
parallel and nondeterministic way. Each guard has a boolean value
followed by a program which may be executed if the guard evaluates to
true. The following shows the main syntax that guards may have.
``` grammar
e ::= if gc fi | do gc od ...
gc ::= (b e) || gc
```
One reason these are interesting language constructs, is because they
allow for the encoding of commands that may be executed when a condition
is true, but that it isn't necessary. Often, when giving instructions,
one does not really specify the order, just the commands that should
eventually be executed.
The guarded commands `gc` will either return a match if a boolean
evaluates to true, or `abort`. There are two constructs that are built
around guarded commands which adds more functionality to them.
`if gc fi` matches one rule in the guarded statement and executes it. If
it does not match a rule, it then acts like `abort`. `do gc od` loops
over the guarded commands while any rule matches. If there no match is
found, it acts like `skip`.
These allow for nice encoding of common algorithms, using two other
constructs that use the guarded commands.
{{< /transclude-2 >}}
{{< /transclude-1 >}}
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">X. Leroy, “Formal certification of
a compiler back-end or: Programming a compiler with a proof assistant,”
in *Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on
principles of programming languages*, in POPL ’06. Charleston, South
Carolina, USA: Association for Computing Machinery, 2006, pp. 42–54.
doi: [10.1145/1111037.1111042].</span>
</div>
<div id="ref-winskel93" class="csl-entry" markdown="1">
<span class="csl-left-margin">\[2\]
</span><span class="csl-right-inline">G. Winskel, *The formal semantics
of programming languages: An introduction*. MIT press, 1993.</span>
</div>
</div>
[\#3a]: /zettel/3a
[10.1145/1111037.1111042]: https://doi.org/10.1145/1111037.1111042
|
