source: etc/campbell/dev-notes/2011-10-12-rtlabs-typing.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: 2.4 KB
Line 
1In Cminor we can attach "typ"s to expressions and have some mild type
2checking.  We'd like the same in RTLabs, but there the statements stand alone
3in the graph so we'll have to be careful to check the type of each register.
4We have the same problem in Cminor for references to variables.
5
6To experiment with this I've been adding typing for unary operations.
7
8First try:
9
10Index the type of statements by the environment and ask for proofs that the
11registers are correctly typed:
12
13  (* A register which has a particular type in the environment. *)
14  definition typreg : (list (register × typ)) → typ → Type[0] ≝
15  λe,t. Σr:register. Exists ? (λx. 〈r,t〉 = x) e.
16 
17  inductive statement (e:list (register × typ)) : Type[0] ≝
18  | St_skip : label → statement e
19...
20  | St_op1 : ∀t,t'. unary_operation t t' → typreg e t → typreg e t' → label → statement e (* destination source *)
21...
22
23The index on the statement type is the usual sort of nuisance - we have to put
24the index in lots of places we'd rather ignore it.  More difficult is that
25when we allocate a fresh register we extend the environment and need to
26rebuild all of the statements with fresh proofs.
27
28This is how the back-end ensures that globals are defined, but they don't
29change during compilation.
30
31---
32
33Second try:
34
35A separate predicate for typing (which I've done as a pattern match rather
36than an inductive relation; should probably try the other), like the other
37invariants.  This looks like it should work reasonably well, but I need to
38sort out the typing of variables in Cminor, because we generate an Oid op
39which isn't well typed otherwise.
40
41
42
43---
44
45Adding type information to variable expressions in Cminor.
46
47Specification isn't hard - change the invariant on the appearance of each
48variable in the parameters or locals lists to include the typ.  But in the
49conversion to Cminor the environment only contains the allocation of the
50variable, so I'll need to add type information here, too.  We also need to
51strengthen the invariant.
52
53This all goes fine, but then I need to retain the types of temporaries, but
54to show this is all OK I need to know that temporaries are fresh for the
55existing variables.  I've cheated and left the previous result as an axiom for
56now, although this means that testing won't work.
57
58The source-language invariant in Cminor/toRTLabs needs strengthened now to
59include something about the types.
Note: See TracBrowser for help on using the repository browser.