source: src/Cminor/toRTLabs.ma @ 764

Last change on this file since 764 was 764, checked in by campbell, 10 years ago

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

File size: 1.2 KB
Line 
1include "common/Globalenvs.ma".
2include "Cminor/syntax.ma".
3include "RTLabs/syntax.ma".
4
5definition env ≝ identifier_map SymbolTag register.
6definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝
7λen,gen. foldr ??
8 (λid,rsengen.
9   do 〈rs,en,gen〉 ← rsengen;
10   do 〈r,gen'〉 ← fresh … gen;
11   OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
12
13axiom boo : ∀T:Type[0]. T.
14
15let rec c2ra_stmt (s:stmt) : graph statement ≝
16?.
17@boo qed.
18
19
20definition c2ra_function (*: internal_function → internal_function*) ≝
21λf.
22let labgen ≝ new_universe LabelTag in
23let reggen0 ≝ new_universe RegisterTag in
24do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
25do 〈locals, env2, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
26do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env2 id)) (f_ptrs f);
27  OK ? (mk_internal_function
28    labgen
29    reggen1
30    (f_sig f)
31    ?
32    params
33    locals
34    ptrs
35    (f_stacksize f)
36    (c2ra_stmt (f_body f))
37    ?
38    ?)
39. @boo qed.
40
41definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
42transform_partial_program ???
43  (transf_partial_fundef ?? c2ra_function).
Note: See TracBrowser for help on using the repository browser.