source: src/joint/Joint.ma @ 1471

Last change on this file since 1471 was 1471, checked in by mulligan, 10 years ago

finished erasure and generalised so as to work on arbitrary joint programs

File size: 7.4 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
6include "common/Graphs.ma".
7
8record params__: Type[1] ≝
9 { acc_a_reg: Type[0]
10 ; acc_b_reg: Type[0]
11 ; dpl_reg: Type[0]
12 ; dph_reg: Type[0]
13 ; pair_reg: Type[0]
14 ; generic_reg: Type[0]
15 ; call_args: Type[0]
16 ; call_dest: Type[0]
17 
18 ; extend_statements: Type[0]
19 }.
20
21record params_: Type[1] ≝
22 { pars__:> params__
23 ; succ: Type[0]
24 }.
25
26(* One common instantiation of params via Graphs of joint_statements
27   (all languages but LIN) *)
28definition graph_params_ : params__ → params_ ≝
29 λpars__. mk_params_ pars__ label.
30
31inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
32  | COMMENT: String → joint_instruction p globals
33  | COST_LABEL: costlabel → joint_instruction p globals
34  | INT: generic_reg p → Byte → joint_instruction p globals
35  | MOVE: pair_reg p → joint_instruction p globals
36  | POP: acc_a_reg p → joint_instruction p globals
37  | PUSH: acc_a_reg p → joint_instruction p globals
38  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
39  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
40  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
41  | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
42  | CLEAR_CARRY: joint_instruction p globals
43  | SET_CARRY: joint_instruction p globals
44  | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
45  | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
46  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
47  | COND: acc_a_reg p → label → joint_instruction p globals
48  | extension: extend_statements p → joint_instruction p globals.
49
50inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
51  | sequential: joint_instruction p globals → succ p → joint_statement p globals
52  | GOTO: label → joint_statement p globals
53  | RETURN: joint_statement p globals.
54
55record params0: Type[1] ≝
56 { pars__' :> params__
57 ; resultT: Type[0]
58 ; paramsT: Type[0]
59 }.
60
61record params1 : Type[1] ≝
62 { pars0 :> params0
63 ; localsT: Type[0]
64 }.
65
66record params (globals: list ident): Type[1] ≝
67 { succ_ : Type[0]
68 ; pars1 :> params1
69 ; codeT: Type[0]
70 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
71 }.
72 
73definition params__of_params: ∀globals. params globals → params_ ≝
74 λglobals,pars. mk_params_ pars (succ_ … pars).
75coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
76 on _p: params ? to params_.
77
78include alias "common/Graphs.ma". (* To pick the right lookup *)
79
80(* One common instantiation of params via Graphs of joint_statements
81   (all languages but LIN) *)
82definition graph_params: params1 → ∀globals: list ident. params globals ≝
83 λpars1,globals.
84  mk_params globals label pars1
85   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
86
87
88(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
89definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
90definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
91
92record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
93{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
94  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
95(*  joint_if_sig: signature;  -- dropped in front end *)
96  joint_if_result   : resultT p;
97  joint_if_params   : paramsT p;
98  joint_if_locals   : localsT p;
99(*CSC: XXXXX stacksize unused for LTL-...*)
100  joint_if_stacksize: nat;
101  joint_if_code     : codeT … p;
102(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
103  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
104(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
105  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
106}.
107
108(* Currified form *)
109definition set_joint_if_exit ≝
110  λglobals,pars.
111  λexit: label.
112  λp:joint_internal_function globals pars.
113  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
114   mk_joint_internal_function globals pars
115    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
116    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
117    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
118
119definition set_joint_code ≝
120  λglobals: list ident.
121  λpars: params globals.
122  λint_fun: joint_internal_function globals pars.
123  λgraph: codeT … pars.
124  λentry.
125  λexit.
126    mk_joint_internal_function globals pars
127      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
128      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
129      graph entry exit.
130
131definition set_joint_if_graph ≝
132  λglobals,pars.
133  λgraph.
134  λp:joint_internal_function globals pars.
135  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
136  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
137    set_joint_code globals pars p graph
138      (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
139
140definition set_luniverse ≝
141  λglobals,pars.
142  λp : joint_internal_function globals pars.
143  λluniverse: universe LabelTag.
144   mk_joint_internal_function globals pars
145    luniverse (joint_if_runiverse … p) (joint_if_result … p)
146    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
147    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
148
149definition set_runiverse ≝
150  λglobals,pars.
151  λp : joint_internal_function globals pars.
152  λruniverse: universe RegisterTag.
153   mk_joint_internal_function globals pars
154    (joint_if_luniverse … p) runiverse (joint_if_result … p)
155    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
156    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
157
158(* Specialized for graph_params *)
159definition add_graph ≝
160  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
161   let code ≝ add … (joint_if_code ?? p) l stmt in
162    mk_joint_internal_function … (graph_params … globals)
163     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
164     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
165     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
166  normalize nodelta;
167  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
168  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
169qed.
170
171definition set_locals ≝
172  λglobals,pars.
173  λp : joint_internal_function globals pars.
174  λlocals.
175   mk_joint_internal_function globals pars
176    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
177    (joint_if_params … p) locals (joint_if_stacksize … p)
178    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
179
180definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
181
182definition joint_program ≝
183 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
Note: See TracBrowser for help on using the repository browser.