source: src/joint/Joint.ma @ 1380

Last change on this file since 1380 was 1380, checked in by sacerdot, 9 years ago

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

File size: 7.1 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_if_graph ≝
120  λglobals,pars.
121  λgraph.
122  λp:joint_internal_function globals pars.
123  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
124  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
125   mk_joint_internal_function globals pars
126    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
127    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
128    graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
129
130definition set_luniverse ≝
131  λglobals,pars.
132  λp : joint_internal_function globals pars.
133  λluniverse: universe LabelTag.
134   mk_joint_internal_function globals pars
135    luniverse (joint_if_runiverse … p) (joint_if_result … p)
136    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
137    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
138
139definition set_runiverse ≝
140  λglobals,pars.
141  λp : joint_internal_function globals pars.
142  λruniverse: universe RegisterTag.
143   mk_joint_internal_function globals pars
144    (joint_if_luniverse … p) runiverse (joint_if_result … p)
145    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
146    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
147
148(* Specialized for graph_params *)
149definition add_graph ≝
150  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
151   let code ≝ add … (joint_if_code ?? p) l stmt in
152    mk_joint_internal_function … (graph_params … globals)
153     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
154     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
155     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
156  normalize nodelta;
157  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
158  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
159qed.
160
161definition set_locals ≝
162  λglobals,pars.
163  λp : joint_internal_function globals pars.
164  λlocals.
165   mk_joint_internal_function globals pars
166    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
167    (joint_if_params … p) locals (joint_if_stacksize … p)
168    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
169
170definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
171
172definition joint_program ≝
173 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
Note: See TracBrowser for help on using the repository browser.