source: etc/campbell/dev-notes/2012-01-19-non-terminating-traces.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 1.1 KB
Line 
1Producing the structured trace for a non-terminating function requires
2building some finite sections.  Depending on whether the next "interesting"
3state in a non-terminating is a label or a call to a non-terminating function
4we need to construct a [trace_label_label] or a [trace_label_call],
5corresponding to the [tld_step] and [tld_base] constructors.
6
7So we walk forward through the trace (recursing on the witness to the fact
8that the trace is "soundly labelled") and
9
10  - if we encounter a labelled state start returning, building a
11    [trace_label_label] as we go (it would be nice to use the existing
12    function, but that would probably be more rather than less work;
13
14  - if we encounter a function call ask the excluded middle whether the call
15    will terminate; if it does then recurse and use [make_label_return] to
16    build the trace_label_return that whatever result will require, if it
17    doesn't then start return a [trace_label_call] (via a [trace_any_call]);
18
19  - otherwise just recurse, then add the appropriate step to whichever type of
20    trace is returned.
Note: See TracBrowser for help on using the repository browser.