source: src/joint/Joint.ma @ 1255

Last change on this file since 1255 was 1255, checked in by sacerdot, 8 years ago

Major mistake fixed: op1 and op2 were assuming the source and dest registers
to be always the same. This is true only from LTL on.

File size: 6.1 KB
RevLine 
[733]1include "ASM/I8051.ma".
[757]2include "common/CostLabel.ma".
[733]3include "common/AST.ma".
[757]4include "common/Registers.ma".
[1252]5include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
[1176]6include "common/Graphs.ma".
[733]7
[1246]8record params__: Type[1] ≝
[1233]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]
[1176]15 
[1233]16 ; extend_statements: Type[0]
[1176]17 
[1233]18 ; resultT: Type[0]
19 ; localsT: Type[0]
20 ; paramsT: Type[0]
21 }.
[1164]22
[1246]23record params_: Type[1] ≝
24 { pars__:> params__
[1233]25 ; succ: Type[0]
26 }.
27
[1246]28inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
[1169]29  | joint_instr_comment: String → joint_instruction p globals
30  | joint_instr_cost_label: costlabel → joint_instruction p globals
31  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
32  | joint_instr_move: pair_reg p → joint_instruction p globals
33  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
34  | joint_instr_push: acc_a_reg p → joint_instruction p globals
35  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
36  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
[1255]37  | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
38  | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
[1169]39  | joint_instr_clear_carry: joint_instruction p globals
40  | joint_instr_set_carry: joint_instruction p globals
41  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
42  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
43  | joint_instr_call_id: ident → nat → joint_instruction p globals
[1250]44  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
45  | joint_instr_extension: extend_statements p → joint_instruction p globals.
[733]46
[1246]47inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
[1233]48  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
[1182]49  | joint_st_goto: label → joint_statement p globals
[1250]50  | joint_st_return: joint_statement p globals.
[1169]51
[1250]52
[1246]53record params (globals: list ident): Type[1] ≝
54 { pars_:> params_
55 ; codeT: Type[0]
56 ; lookup: codeT → label → option (joint_statement pars_ globals)
57 }.
58
[1252]59include alias "common/Graphs.ma". (* To pick the right lookup *)
60
61(* One common instantiation of params via Graphs of joint_statements *)
62definition graph_params: params_ → ∀globals: list ident. params globals ≝
63 λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …).
64
[1246]65record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
[1176]66{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
67  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
68(*  joint_if_sig: signature;  -- dropped in front end *)
[1233]69  joint_if_result   : resultT p;
70  joint_if_params   : paramsT p;
71  joint_if_locals   : localsT p;
[1236]72(*CSC: XXXXX stacksize unused for LTL-...*)
[1176]73  joint_if_stacksize: nat;
[1246]74  joint_if_code     : codeT … p;
[1236]75(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
[1246]76  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
[1236]77(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
[1246]78  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
[1176]79}.
80
[1245]81(* Currified form *)
82definition set_joint_if_exit ≝
[1252]83  λglobals,pars.
[1245]84  λexit: label.
[1252]85  λp:joint_internal_function globals pars.
[1246]86  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
[1252]87   mk_joint_internal_function globals pars
[1245]88    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
89    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
[1246]90    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
[1245]91
[1220]92definition set_luniverse ≝
[1252]93  λglobals,pars.
94  λp : joint_internal_function globals pars.
[1220]95  λluniverse: universe LabelTag.
[1252]96   mk_joint_internal_function globals pars
97    luniverse (joint_if_runiverse … p) (joint_if_result … p)
98    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
99    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
[1220]100
[1254]101definition set_runiverse ≝
102  λglobals,pars.
103  λp : joint_internal_function globals pars.
104  λruniverse: universe RegisterTag.
105   mk_joint_internal_function globals pars
106    (joint_if_luniverse … p) runiverse (joint_if_result … p)
107    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
108    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
109
[1252]110(* Specialized for graph_params *)
111definition add_graph ≝
112  λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals).
113   let code ≝ add … (joint_if_code ?? p) l stmt in
114    mk_joint_internal_function … (graph_params pars_ globals)
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     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
118  normalize nodelta;
119  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
120  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
121qed.
122
123definition set_locals ≝
124  λglobals,pars.
125  λp : joint_internal_function globals pars.
126  λlocals.
127   mk_joint_internal_function globals pars
128    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
129    (joint_if_params … p) locals (joint_if_stacksize … p)
130    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
131
[1233]132definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
[1176]133
[1246]134definition joint_program ≝
135 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
[1176]136
137(****************************************************************************)
138
[1169]139(* Used in LTL and LIN *) 
140inductive registers_move: Type[0] ≝
141 | from_acc: Register → registers_move
[1176]142 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.